Library CT.Instance.Functor.ContravariantFunctor

Require Import CT.Category.
Require Import CT.Functor.
Require Import CT.Instance.Category.Opposite.

F : C^op → D. A contravariant functor flips morphisms.

Program Definition ContravariantFunctor (C D : Category) := Functor (C ^op) D.