categories.dual

Require Import
  Relation_Definitions abstract_algebra theory.categories interfaces.functors.

Section contents.

  Context `{c: @Category Object A Aeq Aid Acomp}.

  Instance flipA: Arrows Object := flip A.

  Global Instance: @CatId Object flipA := Aid.
  Global Instance: @CatComp Object flipA := λ _ _ _, flip (Acomp _ _ _).
  Global Instance e: x y, Equiv (flipA x y) := λ x y, Aeq y x.

  Global Instance: (x y: Object), Equivalence (e x y).

  Global Instance: (x y: Object), Setoid (x y) := {}.

  Instance: (x y z: Object), Proper ((=) ==> (=) ==> (=)) (@comp Object flipA _ x y z).

  Global Instance cat: @Category Object flipA _ _ _.

End contents.

Section functors.

Given a functor F: C → D, we have a functor F^op: C^op → D^op

  Context {C D} F `{Functor C (H:=Ce) D (H1:=De) F}.

  Definition fmap_op: @Fmap _ flipA _ flipA F := fun v w => @fmap _ _ _ _ F _ w v.

  Global Instance: Functor F fmap_op.

End functors.