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.
6 Require Import ProductCategories_ch1_6_1.
8 (*******************************************************************************)
9 (* Chapter 7.5: Natural Isomorphisms *)
10 (*******************************************************************************)
13 Class NaturalIsomorphism `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}(F1:Functor C1 C2 Fobj1)(F2:Functor C1 C2 Fobj2) :=
14 { ni_iso : forall A, Fobj1 A ≅ Fobj2 A
15 ; ni_commutes : forall `(f:A~>B), #(ni_iso A) >>> F2 \ f ~~ F1 \ f >>> #(ni_iso B)
17 Implicit Arguments ni_iso [Ob Hom Ob0 Hom0 C1 C2 Fobj1 Fobj2 F1 F2].
18 Implicit Arguments ni_commutes [Ob Hom Ob0 Hom0 C1 C2 Fobj1 Fobj2 F1 F2 A B].
19 (* FIXME: coerce to NaturalTransformation instead *)
20 Coercion ni_iso : NaturalIsomorphism >-> Funclass.
21 Notation "F <~~~> G" := (@NaturalIsomorphism _ _ _ _ _ _ _ _ F G) : category_scope.
23 (* FIXME: Lemma 7.11: natural isos are natural transformations in which every morphism is an iso *)
25 (* every natural iso is invertible, and that inverse is also a natural iso *)
26 Definition ni_inv `(N:NaturalIsomorphism(F1:=F1)(F2:=F2)) : NaturalIsomorphism F2 F1.
27 intros; apply (Build_NaturalIsomorphism _ _ _ _ _ _ _ _ F2 F1 (fun A => iso_inv _ _ (ni_iso N A))).
28 abstract (intros; simpl;
29 set (ni_commutes N f) as qqq;
31 apply iso_shift_left' in qqq;
33 repeat setoid_rewrite <- associativity;
34 setoid_rewrite iso_comp2;
35 setoid_rewrite left_identity;
40 `{C1:Category}`{C2:Category}
41 {Fobj}(F:Functor C1 C2 Fobj)
42 : NaturalIsomorphism F F.
43 intros; apply (Build_NaturalIsomorphism _ _ _ _ _ _ _ _ F F (fun A => iso_id (F A))).
44 abstract (intros; simpl; setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
47 (* two different choices of composition order are naturally isomorphic (strictly, in fact) *)
48 Instance ni_associativity
49 `{C1:Category}`{C2:Category}`{C3:Category}`{C4:Category}
50 {Fobj1}(F1:Functor C1 C2 Fobj1)
51 {Fobj2}(F2:Functor C2 C3 Fobj2)
52 {Fobj3}(F3:Functor C3 C4 Fobj3)
54 ((F1 >>>> F2) >>>> F3) <~~~> (F1 >>>> (F2 >>>> F3)) :=
55 { ni_iso := fun A => iso_id (F3 (F2 (F1 A))) }.
58 setoid_rewrite left_identity;
59 setoid_rewrite right_identity;
63 Definition ni_comp `{C:Category}`{D:Category}
64 {F1Obj}{F1:@Functor _ _ C _ _ D F1Obj}
65 {F2Obj}{F2:@Functor _ _ C _ _ D F2Obj}
66 {F3Obj}{F3:@Functor _ _ C _ _ D F3Obj}
67 (N1:NaturalIsomorphism F1 F2)
68 (N2:NaturalIsomorphism F2 F3)
69 : NaturalIsomorphism F1 F3.
71 destruct N1 as [ ni_iso1 ni_commutes1 ].
72 destruct N2 as [ ni_iso2 ni_commutes2 ].
73 exists (fun A => id_comp (ni_iso1 A) (ni_iso2 A)).
74 abstract (intros; simpl;
75 setoid_rewrite <- associativity;
76 setoid_rewrite <- ni_commutes1;
77 setoid_rewrite associativity;
78 setoid_rewrite <- ni_commutes2;
82 Definition ni_respects
83 `{A:Category}`{B:Category}`{C:Category}
84 {F0obj}{F0:Functor A B F0obj}
85 {F1obj}{F1:Functor A B F1obj}
86 {G0obj}{G0:Functor B C G0obj}
87 {G1obj}{G1:Functor B C G1obj}
88 : (F0 <~~~> F1) -> (G0 <~~~> G1) -> ((F0 >>>> G0) <~~~> (F1 >>>> G1)).
91 destruct psi as [ psi_niso psi_comm ].
92 destruct phi as [ phi_niso phi_comm ].
94 (fun a => id_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;
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.
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].
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)).
129 [ apply left_identity |
131 apply right_identity]).
134 (* every natural iso is invertible, and that inverse is also a natural iso *)
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.
139 destruct N as [ ni_iso ni_commutes ].
140 exists (fun A => iso_inv _ _ (ni_iso A)).
143 set (ni_commutes _ _ f) as qq.
145 apply iso_shift_left' in qq.
147 repeat setoid_rewrite <- associativity.
148 setoid_rewrite iso_comp2.
149 setoid_rewrite left_identity.
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.
161 destruct N1 as [ ni_iso1 ni_commutes1 ].
162 destruct N2 as [ ni_iso2 ni_commutes2 ].
163 exists (fun A => id_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;
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)
179 ((F1 >>>> F2) >>>> F3) ≃ (F1 >>>> (F2 >>>> F3)).
180 exists (fun A => iso_id (F3 (F2 (F1 A)))).
183 setoid_rewrite left_identity;
184 setoid_rewrite right_identity;
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;
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;
204 Definition if_respects
205 `{A:Category}`{B:Category}`{C:Category}
206 {F0obj}{F0:Functor A B F0obj}
207 {F1obj}{F1:Functor A B F1obj}
208 {G0obj}{G0:Functor B C G0obj}
209 {G1obj}{G1:Functor B C G1obj}
210 : (F0 ≃ F1) -> (G0 ≃ G1) -> ((F0 >>>> G0) ≃ (F1 >>>> G1)).
213 destruct psi as [ psi_niso psi_comm ].
214 destruct phi as [ phi_niso phi_comm ].
215 exists (fun a => id_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))).
216 abstract (intros; simpl;
217 setoid_rewrite <- associativity;
218 setoid_rewrite fmor_preserves_comp;
219 setoid_rewrite <- phi_comm;
220 setoid_rewrite <- fmor_preserves_comp;
221 setoid_rewrite associativity;
222 apply comp_respects; try reflexivity;
226 Section ni_prod_comp.
228 `{C1:Category}`{C2:Category}
229 `{D1:Category}`{D2:Category}
230 {F1Obj}{F1:@Functor _ _ C1 _ _ D1 F1Obj}
231 {F2Obj}{F2:@Functor _ _ C2 _ _ D2 F2Obj}
232 `{E1:Category}`{E2:Category}
233 {G1Obj}{G1:@Functor _ _ D1 _ _ E1 G1Obj}
234 {G2Obj}{G2:@Functor _ _ D2 _ _ E2 G2Obj}.
236 Definition ni_prod_comp_iso A : (((F1 >>>> G1) **** (F2 >>>> G2)) A) ≅ (((F1 **** F2) >>>> (G1 **** G2)) A).
238 unfold functor_product_fobj.
243 Lemma ni_prod_comp : (F1 >>>> G1) **** (F2 >>>> G2) <~~~> (F1 **** F2) >>>> (G1 **** G2).
244 refine {| ni_iso := ni_prod_comp_iso |}.
249 setoid_rewrite left_identity.
250 setoid_rewrite right_identity.