1 Generalizable All Variables.
2 Require Import Notations.
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 (* same as ni_commutes, but phrased in terms of inverses *)
23 Lemma ni_commutes' `(ni:NaturalIsomorphism) : forall `(f:A~>B), F2 \ f >>> #(ni_iso ni B)⁻¹ ~~ #(ni_iso ni A)⁻¹ >>> F1 \ f.
24   intros.
25   apply iso_shift_right'.
26   setoid_rewrite <- associativity.
27   symmetry.
28   apply iso_shift_left'.
29   symmetry.
30   apply ni_commutes.
31   Qed.
33 (* FIXME: Lemma 7.11: natural isos are natural transformations in which every morphism is an iso *)
35 (* every natural iso is invertible, and that inverse is also a natural iso *)
36 Definition ni_inv `(N:NaturalIsomorphism(F1:=F1)(F2:=F2)) : NaturalIsomorphism F2 F1.
37   intros; apply (Build_NaturalIsomorphism _ _ _ _ _ _ _ _ F2 F1 (fun A => iso_inv _ _ (ni_iso N A))).
38   abstract (intros; simpl;
39             set (ni_commutes N f) as qqq;
40             symmetry in qqq;
41             apply iso_shift_left' in qqq;
42             setoid_rewrite qqq;
43             repeat setoid_rewrite <- associativity;
44             setoid_rewrite iso_comp2;
45             setoid_rewrite left_identity;
46             reflexivity).
47   Defined.
49 Definition ni_id
50   `{C1:Category}`{C2:Category}
51   {Fobj}(F:Functor C1 C2 Fobj)
52   : NaturalIsomorphism F F.
53   intros; apply (Build_NaturalIsomorphism _ _ _ _ _ _ _ _ F F (fun A => iso_id (F A))).
54   abstract (intros; simpl; setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
55   Defined.
57 (* two different choices of composition order are naturally isomorphic (strictly, in fact) *)
58 Instance ni_associativity
59   `{C1:Category}`{C2:Category}`{C3:Category}`{C4:Category}
60   {Fobj1}(F1:Functor C1 C2 Fobj1)
61   {Fobj2}(F2:Functor C2 C3 Fobj2)
62   {Fobj3}(F3:Functor C3 C4 Fobj3)
63   :
64   ((F1 >>>> F2) >>>> F3) <~~~> (F1 >>>> (F2 >>>> F3)) :=
65   { ni_iso := fun A => iso_id (F3 (F2 (F1 A))) }.
66   abstract (intros;
67             simpl;
68             setoid_rewrite left_identity;
69             setoid_rewrite right_identity;
70             reflexivity).
71   Defined.
73 Definition ni_comp `{C:Category}`{D:Category}
74    {F1Obj}{F1:@Functor _ _ C _ _ D F1Obj}
75    {F2Obj}{F2:@Functor _ _ C _ _ D F2Obj}
76    {F3Obj}{F3:@Functor _ _ C _ _ D F3Obj}
77    (N1:NaturalIsomorphism F1 F2)
78    (N2:NaturalIsomorphism F2 F3)
79    : NaturalIsomorphism F1 F3.
80    intros.
81      destruct N1 as [ ni_iso1 ni_commutes1 ].
82      destruct N2 as [ ni_iso2 ni_commutes2 ].
83    exists (fun A => iso_comp (ni_iso1 A) (ni_iso2 A)).
84    abstract (intros; simpl;
85              setoid_rewrite <- associativity;
86              setoid_rewrite <- ni_commutes1;
87              setoid_rewrite associativity;
88              setoid_rewrite <- ni_commutes2;
89              reflexivity).
90    Defined.
92 Definition ni_respects1
93   `{A:Category}`{B:Category}
94   {Fobj}(F:Functor A B Fobj)
95   `{C:Category}
96   {G0obj}(G0:Functor B C G0obj)
97   {G1obj}(G1:Functor B C G1obj)
98   : (G0 <~~~> G1) -> ((F >>>> G0) <~~~> (F >>>> G1)).
99   intro phi.
100   destruct phi as [ phi_niso phi_comm ].
101   refine {| ni_iso := (fun a => phi_niso (Fobj a)) |}.
102   intros; simpl; apply phi_comm.
103   Defined.
105 Definition ni_respects2
106   `{A:Category}`{B:Category}
107   {F0obj}(F0:Functor A B F0obj)
108   {F1obj}(F1:Functor A B F1obj)
109   `{C:Category}
110   {Gobj}(G:Functor B C Gobj)
111   : (F0 <~~~> F1) -> ((F0 >>>> G) <~~~> (F1 >>>> G)).
112   intro phi.
113   destruct phi as [ phi_niso phi_comm ].
114   refine {| ni_iso := fun a => (@functors_preserve_isos _ _ _ _ _ _ _ G) _ _ (phi_niso a) |}.
115   intros; simpl.
116   setoid_rewrite fmor_preserves_comp.
117   apply fmor_respects.
118   apply phi_comm.
119   Defined.
121 Definition ni_respects
122   `{A:Category}`{B:Category}
123   {F0obj}(F0:Functor A B F0obj)
124   {F1obj}(F1:Functor A B F1obj)
125   `{C:Category}
126   {G0obj}(G0:Functor B C G0obj)
127   {G1obj}(G1:Functor B C G1obj)
128   : (F0 <~~~> F1) -> (G0 <~~~> G1) -> ((F0 >>>> G0) <~~~> (F1 >>>> G1)).
129   intro phi.
130   intro psi.
131   destruct psi as [ psi_niso psi_comm ].
132   destruct phi as [ phi_niso phi_comm ].
133   refine {| ni_iso :=
134       (fun a => iso_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))) |}.
135   abstract (intros; simpl;
136             setoid_rewrite <- associativity;
137             setoid_rewrite fmor_preserves_comp;
138             setoid_rewrite <- phi_comm;
139             setoid_rewrite <- fmor_preserves_comp;
140             setoid_rewrite associativity;
141             apply comp_respects; try reflexivity;
142             apply psi_comm).
143   Defined.
145 (*
146  * Some structures (like monoidal and premonoidal functors) use the isomorphism
147  * component of a natural isomorphism in an "informative" way; these structures
148  * should use NaturalIsomorphism.
149  *
150  * However, in other situations the actual iso used is irrelevant; all
151  * that matters is the fact that a natural family of them exists.  In
152  * these cases we can speed up Coq (and the extracted program)
153  * considerably by making the family of isos belong to [Prop] rather
154  * than [Type].  IsomorphicFunctors does this -- it's essentially a
155  * copy of NaturalIsomorphism which lives in [Prop].
156  *)
158 (* Definition 7.10 *)
159 Definition IsomorphicFunctors `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}(F1:Functor C1 C2 Fobj1)(F2:Functor C1 C2 Fobj2) :=
160   exists  ni_iso      : (forall A, Fobj1 A ≅ Fobj2 A),
161                          forall `(f:A~>B), #(ni_iso A) >>> F2 \ f ~~ F1 \ f >>> #(ni_iso B).
162 Notation "F ≃ G" := (@IsomorphicFunctors _ _ _ _ _ _ _ _ F G) : category_scope.
164 Definition if_id `{C:Category}`{D:Category}{Fobj}(F:Functor C D Fobj) : IsomorphicFunctors F F.
165   exists (fun A => iso_id (F A)).
166   abstract (intros;
167             simpl;
168             etransitivity;
169             [ apply left_identity |
170             symmetry;
171             apply right_identity]).
172   Qed.
174 (* every natural iso is invertible, and that inverse is also a natural iso *)
175 Definition if_inv
176   `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}{F1:Functor C1 C2 Fobj1}{F2:Functor C1 C2 Fobj2}
177    (N:IsomorphicFunctors F1 F2) : IsomorphicFunctors F2 F1.
178   intros.
179     destruct N as [ ni_iso ni_commutes ].
180     exists (fun A => iso_inv _ _ (ni_iso A)).
181   intros; simpl.
182     symmetry.
183     set (ni_commutes _ _ f) as qq.
184     symmetry in qq.
185     apply iso_shift_left' in qq.
186     setoid_rewrite qq.
187     repeat setoid_rewrite <- associativity.
188     setoid_rewrite iso_comp2.
189     setoid_rewrite left_identity.
190     reflexivity.
191   Qed.
193 Definition if_comp `{C:Category}`{D:Category}
194    {F1Obj}{F1:@Functor _ _ C _ _ D F1Obj}
195    {F2Obj}{F2:@Functor _ _ C _ _ D F2Obj}
196    {F3Obj}{F3:@Functor _ _ C _ _ D F3Obj}
197    (N1:IsomorphicFunctors F1 F2)
198    (N2:IsomorphicFunctors F2 F3)
199    : IsomorphicFunctors F1 F3.
200    intros.
201      destruct N1 as [ ni_iso1 ni_commutes1 ].
202      destruct N2 as [ ni_iso2 ni_commutes2 ].
203    exists (fun A => iso_comp (ni_iso1 A) (ni_iso2 A)).
204    abstract (intros; simpl;
205              setoid_rewrite <- associativity;
206              setoid_rewrite <- ni_commutes1;
207              setoid_rewrite associativity;
208              setoid_rewrite <- ni_commutes2;
209              reflexivity).
210    Qed.
212 (* two different choices of composition order are naturally isomorphic (strictly, in fact) *)
213 Definition if_associativity
214   `{C1:Category}`{C2:Category}`{C3:Category}`{C4:Category}
215   {Fobj1}(F1:Functor C1 C2 Fobj1)
216   {Fobj2}(F2:Functor C2 C3 Fobj2)
217   {Fobj3}(F3:Functor C3 C4 Fobj3)
218   :
219   ((F1 >>>> F2) >>>> F3) ≃ (F1 >>>> (F2 >>>> F3)).
220   exists (fun A => iso_id (F3 (F2 (F1 A)))).
221   abstract (intros;
222             simpl;
223             setoid_rewrite left_identity;
224             setoid_rewrite right_identity;
225             reflexivity).
226   Defined.
228 Definition if_left_identity `{C1:Category}`{C2:Category} {Fobj1}(F1:Functor C1 C2 Fobj1) : (functor_id _ >>>> F1) ≃ F1.
229   exists (fun a => iso_id (F1 a)).
230   abstract (intros; unfold functor_comp; simpl;
231             setoid_rewrite left_identity;
232             setoid_rewrite right_identity;
233             reflexivity).
234   Defined.
236 Definition if_right_identity `{C1:Category}`{C2:Category} {Fobj1}(F1:Functor C1 C2 Fobj1) : (F1 >>>> functor_id _) ≃ F1.
237   exists (fun a => iso_id (F1 a)).
238   abstract (intros; unfold functor_comp; simpl;
239             setoid_rewrite left_identity;
240             setoid_rewrite right_identity;
241             reflexivity).
242   Defined.
244 Definition if_respects
245   `{A:Category}`{B:Category}
246   {F0obj}(F0:Functor A B F0obj)
247   {F1obj}(F1:Functor A B F1obj)
248   `{C:Category}
249   {G0obj}(G0:Functor B C G0obj)
250   {G1obj}(G1:Functor B C G1obj)
251   : (F0 ≃ F1) -> (G0 ≃ G1) -> ((F0 >>>> G0) ≃ (F1 >>>> G1)).
252   intro phi.
253   intro psi.
254   destruct psi as [ psi_niso psi_comm ].
255   destruct phi as [ phi_niso phi_comm ].
256   exists (fun a => iso_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))).
257   abstract (intros; simpl;
258             setoid_rewrite <- associativity;
259             setoid_rewrite fmor_preserves_comp;
260             setoid_rewrite <- phi_comm;
261             setoid_rewrite <- fmor_preserves_comp;
262             setoid_rewrite associativity;
263             apply comp_respects; try reflexivity;
264             apply psi_comm).
265   Defined.
267 Section ni_prod_comp.
268 Require Import ProductCategories_ch1_6_1.
269   Context
270   `{C1:Category}`{C2:Category}
271   `{D1:Category}`{D2:Category}
272    {F1Obj}(F1:@Functor _ _ C1 _ _ D1 F1Obj)
273    {F2Obj}(F2:@Functor _ _ C2 _ _ D2 F2Obj)
274   `{E1:Category}`{E2:Category}
275    {G1Obj}(G1:@Functor _ _ D1 _ _ E1 G1Obj)
276    {G2Obj}(G2:@Functor _ _ D2 _ _ E2 G2Obj).
278   Definition ni_prod_comp_iso A : (((F1 >>>> G1) **** (F2 >>>> G2)) A) ≅ (((F1 **** F2) >>>> (G1 **** G2)) A).
279     unfold functor_fobj.
280     unfold functor_product_fobj.
281     simpl.
282     apply iso_id.
283     Defined.
285   Lemma ni_prod_comp : (F1 >>>> G1) **** (F2 >>>> G2) <~~~> (F1 **** F2) >>>> (G1 **** G2).
286     refine {| ni_iso := ni_prod_comp_iso |}.
287     intros.
288     destruct A.
289     destruct B.
290     simpl.
291     setoid_rewrite left_identity.
292     setoid_rewrite right_identity.
293     split; reflexivity.
294     Defined.
295 End ni_prod_comp.