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.
7 (******************************************************************************)
8 (* Chapter 1.6.2: Opposite Categories                                         *)
9 (******************************************************************************)
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).
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.
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.
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.
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.
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.