Library Duals


Require Import Utf8.
Require Import JMeq Eqdep.
Require Export Category CategoryIsomorphisms Functor.
Require Import Common Notations.

Set Implicit Arguments.

Generalizable All Variables.

Dual Categories


Local Open Scope category_scope.

Section OppositeCategory.
  Definition OppositeCategory `(C : @Category objC) : @Category objC
    := @Build_Category objC
                       (fun s dMorphism C d s)
                       (@Identity _ C)
                       (fun _ _ _ m1 m2 ⇒ @Compose _ C _ _ _ m2 m1)
                       (fun _ _ _ _ _ _ _eq_sym (@Associativity _ _ _ _ _ _ _ _ _))
                       (fun _ _ ⇒ @RightIdentity _ _ _ _)
                       (fun _ _ ⇒ @LeftIdentity _ _ _ _).
End OppositeCategory.


Section OppositeFunctor.
  Context `(C : @Category objC).
  Context `(D : @Category objD).
  Variable F : Functor C D.
  Let COp := OppositeCategory C.
  Let DOp := OppositeCategory D.

  Definition OppositeFunctor : Functor COp DOp
    := Build_Functor COp DOp
                     (fun c : COpF c : DOp)
                     (fun (s d : COp) (m : C.(Morphism) d s) ⇒ MorphismOf F (s := d) (d := s) m)
                     (fun d' d s m1 m2FCompositionOf F s d d' m2 m1)
                     (FIdentityOf F).
End OppositeFunctor.