src/OppositeCategories_ch1_6_2.v

   1 Generalizable All Variables.
   2 Require Import Preamble.
   3 Require Import Categories_ch1_3.
   4 Require Import Functors_ch1_4.
   5 Require Import Isomorphisms_ch1_5.
   6
   7 (******************************************************************************)
   8 (* Chapter 1.6.2: Opposite Categories                                         *)
   9 (******************************************************************************)
  10
  11 (* we don't want to register this as an instance, because it will confuse Coq *)
  12 Definition Opposite `(C:@Category Ob Hom) : Category Ob (fun x y => Hom y x).
  13   intros.
  14   apply (Build_Category Ob (fun x y => Hom y x)) with
  15     (id    := fun a         => @id    _ _ C a)
  16     (comp  := fun a b c f g => @comp  _ _ C c b a g f)
  17     (eqv   := fun a b   f g => @eqv   _ _ C b a f g).
  18
  19   intros; apply Build_Equivalence;
  20     [ unfold Reflexive;  intros; reflexivity
  21     | unfold Symmetric;  intros; symmetry; auto
  22     | unfold Transitive; intros; transitivity y; auto
  23     ].
  24   unfold Proper. intros. unfold respectful. intros. setoid_rewrite H. setoid_rewrite H0. reflexivity.
  25   intros; apply (@right_identity _ _ C).
  26   intros; apply (@left_identity _ _ C).
  27   intros. symmetry; apply associativity.
  28   Defined.
  29 Notation "C ⁽ºᑭ⁾" := (Opposite C)  : category_scope.
  30
  31 (* every functor between two categories determines a functor between their opposites *)
  32 Definition func_op `(F:Functor(c1:=c1)(c2:=c2)(fobj:=fobj)) : Functor c1⁽ºᑭ⁾ c2⁽ºᑭ⁾ fobj.
  33   apply (@Build_Functor _ _ c1⁽ºᑭ⁾ _ _ c2⁽ºᑭ⁾ fobj (fun a b f => fmor F f)).
  34   abstract (intros; apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H)).
  35   abstract (intros; apply (@fmor_preserves_id _ _ _ _ _ _ _ F a)).
  36   abstract (intros; apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f)).
  37   Defined.
  38
  39 (* we could do this by simply showing that (Opposite (Opposite C)) is isomorphic to C, but Coq distinguishes between
  40  * two categories being *equal* versus merely isomorphic, so it's handy to be able to do this *)
  41 Definition func_opop `{c1:Category}`{c2:Category}{fobj}(F:Functor c1⁽ºᑭ⁾ c2⁽ºᑭ⁾ fobj) : Functor c1 c2 fobj.
  42   apply (@Build_Functor _ _ c1 _ _ c2 fobj (fun a b f => fmor F f)).
  43   abstract (intros; apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H)).
  44   abstract (intros; apply (@fmor_preserves_id _ _ _ _ _ _ _ F a)).
  45   abstract (intros; apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f)).
  46   Defined.
  47
  48 Definition func_op1 `{c1:Category}`{c2:Category}{fobj}(F:Functor c1⁽ºᑭ⁾ c2 fobj) : Functor c1 c2⁽ºᑭ⁾ fobj.
  49   apply (@Build_Functor _ _ c1 _ _ c2⁽ºᑭ⁾ fobj (fun a b f => fmor F f)).
  50   abstract (intros; apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H)).
  51   abstract (intros; apply (@fmor_preserves_id _ _ _ _ _ _ _ F a)).
  52   abstract (intros; apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f)).
  53   Defined.
  54
  55 Definition func_op2 `{c1:Category}`{c2:Category}{fobj}(F:Functor c1 c2⁽ºᑭ⁾ fobj) : Functor c1⁽ºᑭ⁾ c2 fobj.
  56   apply (@Build_Functor _ _ c1⁽ºᑭ⁾ _ _ c2 fobj (fun a b f => fmor F f)).
  57   abstract (intros; apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H)).
  58   abstract (intros; apply (@fmor_preserves_id _ _ _ _ _ _ _ F a)).
  59   abstract (intros; apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f)).
  60   Defined.
  61