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 (*******************************************************************************)
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)
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.
25 apply iso_shift_right'.
26 setoid_rewrite <- associativity.
28 apply iso_shift_left'.
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;
41 apply iso_shift_left' in qqq;
43 repeat setoid_rewrite <- associativity;
44 setoid_rewrite iso_comp2;
45 setoid_rewrite left_identity;
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).
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)
64 ((F1 >>>> F2) >>>> F3) <~~~> (F1 >>>> (F2 >>>> F3)) :=
65 { ni_iso := fun A => iso_id (F3 (F2 (F1 A))) }.
68 setoid_rewrite left_identity;
69 setoid_rewrite right_identity;
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.
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;
92 Definition ni_respects1
93 `{A:Category}`{B:Category}
94 {Fobj}(F:Functor A B Fobj)
96 {G0obj}(G0:Functor B C G0obj)
97 {G1obj}(G1:Functor B C G1obj)
98 : (G0 <~~~> G1) -> ((F >>>> G0) <~~~> (F >>>> G1)).
100 destruct phi as [ phi_niso phi_comm ].
101 refine {| ni_iso := (fun a => phi_niso (Fobj a)) |}.
102 intros; simpl; apply phi_comm.
105 Definition ni_respects2
106 `{A:Category}`{B:Category}
107 {F0obj}(F0:Functor A B F0obj)
108 {F1obj}(F1:Functor A B F1obj)
110 {Gobj}(G:Functor B C Gobj)
111 : (F0 <~~~> F1) -> ((F0 >>>> G) <~~~> (F1 >>>> G)).
113 destruct phi as [ phi_niso phi_comm ].
114 refine {| ni_iso := fun a => (@functors_preserve_isos _ _ _ _ _ _ _ G) _ _ (phi_niso a) |}.
116 setoid_rewrite fmor_preserves_comp.
121 Definition ni_respects
122 `{A:Category}`{B:Category}
123 {F0obj}(F0:Functor A B F0obj)
124 {F1obj}(F1:Functor A B F1obj)
126 {G0obj}(G0:Functor B C G0obj)
127 {G1obj}(G1:Functor B C G1obj)
128 : (F0 <~~~> F1) -> (G0 <~~~> G1) -> ((F0 >>>> G0) <~~~> (F1 >>>> G1)).
131 destruct psi as [ psi_niso psi_comm ].
132 destruct phi as [ phi_niso phi_comm ].
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;
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.
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].
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)).
169 [ apply left_identity |
171 apply right_identity]).
174 (* every natural iso is invertible, and that inverse is also a natural iso *)
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.
179 destruct N as [ ni_iso ni_commutes ].
180 exists (fun A => iso_inv _ _ (ni_iso A)).
183 set (ni_commutes _ _ f) as qq.
185 apply iso_shift_left' in qq.
187 repeat setoid_rewrite <- associativity.
188 setoid_rewrite iso_comp2.
189 setoid_rewrite left_identity.
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.
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;
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)
219 ((F1 >>>> F2) >>>> F3) ≃ (F1 >>>> (F2 >>>> F3)).
220 exists (fun A => iso_id (F3 (F2 (F1 A)))).
223 setoid_rewrite left_identity;
224 setoid_rewrite right_identity;
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;
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;
244 Definition if_respects
245 `{A:Category}`{B:Category}
246 {F0obj}(F0:Functor A B F0obj)
247 {F1obj}(F1:Functor A B F1obj)
249 {G0obj}(G0:Functor B C G0obj)
250 {G1obj}(G1:Functor B C G1obj)
251 : (F0 ≃ F1) -> (G0 ≃ G1) -> ((F0 >>>> G0) ≃ (F1 >>>> G1)).
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;
267 Section ni_prod_comp.
268 Require Import ProductCategories_ch1_6_1.
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).
280 unfold functor_product_fobj.
285 Lemma ni_prod_comp : (F1 >>>> G1) **** (F2 >>>> G2) <~~~> (F1 **** F2) >>>> (G1 **** G2).
286 refine {| ni_iso := ni_prod_comp_iso |}.
291 setoid_rewrite left_identity.
292 setoid_rewrite right_identity.