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 7.5: Natural Isomorphisms                                           *)
9 (*******************************************************************************)
11 (* Definition 7.10 *)
12 Class NaturalIsomorphism `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}(F1:Functor C1 C2 Fobj1)(F2:Functor C1 C2 Fobj2) :=
13 { ni_iso      : forall A, Fobj1 A ≅ Fobj2 A
14 ; ni_commutes : forall `(f:A~>B), #(ni_iso A) >>> F2 \ f ~~ F1 \ f >>> #(ni_iso B)
15 }.
16 Implicit Arguments ni_iso      [Ob Hom Ob0 Hom0 C1 C2 Fobj1 Fobj2 F1 F2].
17 Implicit Arguments ni_commutes [Ob Hom Ob0 Hom0 C1 C2 Fobj1 Fobj2 F1 F2 A B].
18 (* FIXME: coerce to NaturalTransformation instead *)
19 Coercion ni_iso : NaturalIsomorphism >-> Funclass.
20 Notation "F <~~~> G" := (@NaturalIsomorphism _ _ _ _ _ _ _ _ F G) : category_scope.
22 (* FIXME: Lemma 7.11: natural isos are natural transformations in which every morphism is an iso *)
24 (* every natural iso is invertible, and that inverse is also a natural iso *)
25 Definition ni_inv `(N:NaturalIsomorphism(F1:=F1)(F2:=F2)) : NaturalIsomorphism F2 F1.
26   intros; apply (Build_NaturalIsomorphism _ _ _ _ _ _ _ _ F2 F1 (fun A => iso_inv _ _ (ni_iso N A))).
27   abstract (intros; simpl;
28             set (ni_commutes N f) as qqq;
29             symmetry in qqq;
30             apply iso_shift_left' in qqq;
31             setoid_rewrite qqq;
32             repeat setoid_rewrite <- associativity;
33             setoid_rewrite iso_comp2;
34             setoid_rewrite left_identity;
35             reflexivity).
36   Defined.
38 Definition ni_id
39   `{C1:Category}`{C2:Category}
40   {Fobj}(F:Functor C1 C2 Fobj)
41   : NaturalIsomorphism F F.
42   intros; apply (Build_NaturalIsomorphism _ _ _ _ _ _ _ _ F F (fun A => iso_id (F A))).
43   abstract (intros; simpl; setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
44   Defined.
46 (* two different choices of composition order are naturally isomorphic (strictly, in fact) *)
47 Instance ni_associativity
48   `{C1:Category}`{C2:Category}`{C3:Category}`{C4:Category}
49   {Fobj1}(F1:Functor C1 C2 Fobj1)
50   {Fobj2}(F2:Functor C2 C3 Fobj2)
51   {Fobj3}(F3:Functor C3 C4 Fobj3)
52   :
53   ((F1 >>>> F2) >>>> F3) <~~~> (F1 >>>> (F2 >>>> F3)) :=
54   { ni_iso := fun A => iso_id (F3 (F2 (F1 A))) }.
55   abstract (intros;
56             simpl;
57             setoid_rewrite left_identity;
58             setoid_rewrite right_identity;
59             reflexivity).
60   Defined.
62 Definition ni_comp `{C:Category}`{D:Category}
63    {F1Obj}{F1:@Functor _ _ C _ _ D F1Obj}
64    {F2Obj}{F2:@Functor _ _ C _ _ D F2Obj}
65    {F3Obj}{F3:@Functor _ _ C _ _ D F3Obj}
66    (N1:NaturalIsomorphism F1 F2)
67    (N2:NaturalIsomorphism F2 F3)
68    : NaturalIsomorphism F1 F3.
69    intros.
70      destruct N1 as [ ni_iso1 ni_commutes1 ].
71      destruct N2 as [ ni_iso2 ni_commutes2 ].
72    exists (fun A => iso_comp (ni_iso1 A) (ni_iso2 A)).
73    abstract (intros; simpl;
74              setoid_rewrite <- associativity;
75              setoid_rewrite <- ni_commutes1;
76              setoid_rewrite associativity;
77              setoid_rewrite <- ni_commutes2;
78              reflexivity).
79    Defined.
81 Definition ni_respects
82   `{A:Category}`{B:Category}
83   {F0obj}(F0:Functor A B F0obj)
84   {F1obj}(F1:Functor A B F1obj)
85   `{C:Category}
86   {G0obj}(G0:Functor B C G0obj)
87   {G1obj}(G1:Functor B C G1obj)
88   : (F0 <~~~> F1) -> (G0 <~~~> G1) -> ((F0 >>>> G0) <~~~> (F1 >>>> G1)).
89   intro phi.
90   intro psi.
91   destruct psi as [ psi_niso psi_comm ].
92   destruct phi as [ phi_niso phi_comm ].
93   refine {| ni_iso :=
94       (fun a => iso_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))) |}.
95   abstract (intros; simpl;
96             setoid_rewrite <- associativity;
97             setoid_rewrite fmor_preserves_comp;
98             setoid_rewrite <- phi_comm;
99             setoid_rewrite <- fmor_preserves_comp;
100             setoid_rewrite associativity;
101             apply comp_respects; try reflexivity;
102             apply psi_comm).
103   Defined.
105 (*
106  * Some structures (like monoidal and premonoidal functors) use the isomorphism
107  * component of a natural isomorphism in an "informative" way; these structures
108  * should use NaturalIsomorphism.
109  *
110  * However, in other situations the actual iso used is irrelevant; all
111  * that matters is the fact that a natural family of them exists.  In
112  * these cases we can speed up Coq (and the extracted program)
113  * considerably by making the family of isos belong to [Prop] rather
114  * than [Type].  IsomorphicFunctors does this -- it's essentially a
115  * copy of NaturalIsomorphism which lives in [Prop].
116  *)
118 (* Definition 7.10 *)
119 Definition IsomorphicFunctors `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}(F1:Functor C1 C2 Fobj1)(F2:Functor C1 C2 Fobj2) :=
120   exists  ni_iso      : (forall A, Fobj1 A ≅ Fobj2 A),
121                          forall `(f:A~>B), #(ni_iso A) >>> F2 \ f ~~ F1 \ f >>> #(ni_iso B).
122 Notation "F ≃ G" := (@IsomorphicFunctors _ _ _ _ _ _ _ _ F G) : category_scope.
124 Definition if_id `{C:Category}`{D:Category}{Fobj}(F:Functor C D Fobj) : IsomorphicFunctors F F.
125   exists (fun A => iso_id (F A)).
126   abstract (intros;
127             simpl;
128             etransitivity;
129             [ apply left_identity |
130             symmetry;
131             apply right_identity]).
132   Qed.
134 (* every natural iso is invertible, and that inverse is also a natural iso *)
135 Definition if_inv
136   `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}{F1:Functor C1 C2 Fobj1}{F2:Functor C1 C2 Fobj2}
137    (N:IsomorphicFunctors F1 F2) : IsomorphicFunctors F2 F1.
138   intros.
139     destruct N as [ ni_iso ni_commutes ].
140     exists (fun A => iso_inv _ _ (ni_iso A)).
141   intros; simpl.
142     symmetry.
143     set (ni_commutes _ _ f) as qq.
144     symmetry in qq.
145     apply iso_shift_left' in qq.
146     setoid_rewrite qq.
147     repeat setoid_rewrite <- associativity.
148     setoid_rewrite iso_comp2.
149     setoid_rewrite left_identity.
150     reflexivity.
151   Qed.
153 Definition if_comp `{C:Category}`{D:Category}
154    {F1Obj}{F1:@Functor _ _ C _ _ D F1Obj}
155    {F2Obj}{F2:@Functor _ _ C _ _ D F2Obj}
156    {F3Obj}{F3:@Functor _ _ C _ _ D F3Obj}
157    (N1:IsomorphicFunctors F1 F2)
158    (N2:IsomorphicFunctors F2 F3)
159    : IsomorphicFunctors F1 F3.
160    intros.
161      destruct N1 as [ ni_iso1 ni_commutes1 ].
162      destruct N2 as [ ni_iso2 ni_commutes2 ].
163    exists (fun A => iso_comp (ni_iso1 A) (ni_iso2 A)).
164    abstract (intros; simpl;
165              setoid_rewrite <- associativity;
166              setoid_rewrite <- ni_commutes1;
167              setoid_rewrite associativity;
168              setoid_rewrite <- ni_commutes2;
169              reflexivity).
170    Qed.
172 (* two different choices of composition order are naturally isomorphic (strictly, in fact) *)
173 Definition if_associativity
174   `{C1:Category}`{C2:Category}`{C3:Category}`{C4:Category}
175   {Fobj1}(F1:Functor C1 C2 Fobj1)
176   {Fobj2}(F2:Functor C2 C3 Fobj2)
177   {Fobj3}(F3:Functor C3 C4 Fobj3)
178   :
179   ((F1 >>>> F2) >>>> F3) ≃ (F1 >>>> (F2 >>>> F3)).
180   exists (fun A => iso_id (F3 (F2 (F1 A)))).
181   abstract (intros;
182             simpl;
183             setoid_rewrite left_identity;
184             setoid_rewrite right_identity;
185             reflexivity).
186   Defined.
188 Definition if_left_identity `{C1:Category}`{C2:Category} {Fobj1}(F1:Functor C1 C2 Fobj1) : (functor_id _ >>>> F1) ≃ F1.
189   exists (fun a => iso_id (F1 a)).
190   abstract (intros; unfold functor_comp; simpl;
191             setoid_rewrite left_identity;
192             setoid_rewrite right_identity;
193             reflexivity).
194   Defined.
196 Definition if_right_identity `{C1:Category}`{C2:Category} {Fobj1}(F1:Functor C1 C2 Fobj1) : (F1 >>>> functor_id _) ≃ F1.
197   exists (fun a => iso_id (F1 a)).
198   abstract (intros; unfold functor_comp; simpl;
199             setoid_rewrite left_identity;
200             setoid_rewrite right_identity;
201             reflexivity).
202   Defined.
204 Definition if_respects
205   `{A:Category}`{B:Category}
206   {F0obj}(F0:Functor A B F0obj)
207   {F1obj}(F1:Functor A B F1obj)
208   `{C:Category}
209   {G0obj}(G0:Functor B C G0obj)
210   {G1obj}(G1:Functor B C G1obj)
211   : (F0 ≃ F1) -> (G0 ≃ G1) -> ((F0 >>>> G0) ≃ (F1 >>>> G1)).
212   intro phi.
213   intro psi.
214   destruct psi as [ psi_niso psi_comm ].
215   destruct phi as [ phi_niso phi_comm ].
216   exists (fun a => iso_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))).
217   abstract (intros; simpl;
218             setoid_rewrite <- associativity;
219             setoid_rewrite fmor_preserves_comp;
220             setoid_rewrite <- phi_comm;
221             setoid_rewrite <- fmor_preserves_comp;
222             setoid_rewrite associativity;
223             apply comp_respects; try reflexivity;
224             apply psi_comm).
225   Defined.
227 Section ni_prod_comp.
228 Require Import ProductCategories_ch1_6_1.
229   Context
230   `{C1:Category}`{C2:Category}
231   `{D1:Category}`{D2:Category}
232    {F1Obj}(F1:@Functor _ _ C1 _ _ D1 F1Obj)
233    {F2Obj}(F2:@Functor _ _ C2 _ _ D2 F2Obj)
234   `{E1:Category}`{E2:Category}
235    {G1Obj}(G1:@Functor _ _ D1 _ _ E1 G1Obj)
236    {G2Obj}(G2:@Functor _ _ D2 _ _ E2 G2Obj).
238   Definition ni_prod_comp_iso A : (((F1 >>>> G1) **** (F2 >>>> G2)) A) ≅ (((F1 **** F2) >>>> (G1 **** G2)) A).
239     unfold functor_fobj.
240     unfold functor_product_fobj.
241     simpl.
242     apply iso_id.
243     Defined.
245   Lemma ni_prod_comp : (F1 >>>> G1) **** (F2 >>>> G2) <~~~> (F1 **** F2) >>>> (G1 **** G2).
246     refine {| ni_iso := ni_prod_comp_iso |}.
247     intros.
248     destruct A.
249     destruct B.
250     simpl.
251     setoid_rewrite left_identity.
252     setoid_rewrite right_identity.
253     split; reflexivity.
254     Defined.
255 End ni_prod_comp.