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).
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
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.
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)).
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)).
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)).
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)).