1 (*********************************************************************************************************************************)
2 (* ReificationsIsomorphicToGeneralizedArrows: *)
4 (* The category of generalized arrows and the category of reifications are isomorphic categories. *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import Categories_ch1_3.
12 Require Import Functors_ch1_4.
13 Require Import Isomorphisms_ch1_5.
14 Require Import ProductCategories_ch1_6_1.
15 Require Import OppositeCategories_ch1_6_2.
16 Require Import Enrichment_ch2_8.
17 Require Import Subcategories_ch7_1.
18 Require Import NaturalTransformations_ch7_4.
19 Require Import NaturalIsomorphisms_ch7_5.
20 Require Import PreMonoidalCategories.
21 Require Import MonoidalCategories_ch7_8.
22 Require Import Coherence_ch7_8.
23 Require Import RepresentableStructure_ch7_2.
24 Require Import Reification.
25 Require Import GeneralizedArrow.
26 Require Import GeneralizedArrowFromReification.
27 Require Import ReificationFromGeneralizedArrow.
28 Require Import ReificationCategory.
29 Require Import GeneralizedArrowCategory.
30 Require Import ReificationCategory.
31 Require Import ReificationsAndGeneralizedArrows.
32 Require Import WeakFunctorCategory.
33 Require Import BijectionLemma.
34 Require Import Enrichments.
36 Section ReificationsIsomorphicToGeneralizedArrows.
38 Definition M1 {c1 c2 : SMMEs} :
39 (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
40 (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
42 destruct GA; [ apply roi_id | idtac ].
44 apply (reification_from_garrow s1 s2 g).
47 (* I tried really hard to avoid this *)
48 Require Import Coq.Logic.Eqdep.
50 Inductive Heq : forall {A}{B}, A -> B -> Prop :=
51 heq : forall {A} (a:A), Heq a a.
53 Lemma invert_ga' : forall (a b: SMME)
54 (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>b), a=b ->
55 (Heq f (gaoi_id a)) \/ (exists f', Heq f (gaoi_ga a b f')).
64 Lemma invert_ga : forall (a: SMME)
65 (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
66 (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
68 set (invert_ga' a a f (refl_equal a)) as q.
72 apply inj_pairT2 in H2.
73 apply inj_pairT2 in H1.
79 apply inj_pairT2 in H2.
80 apply inj_pairT2 in H1.
84 Lemma invert_reif' : forall (a b: SMME)
85 (f:a~~{MorphismsOfCategoryOfReifications}~~>b), a=b ->
86 (Heq f (roi_id a)) \/ (exists f', Heq f (roi_reif a b f')).
95 Lemma invert_reif : forall (a: SMME)
96 (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
97 (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
99 set (invert_reif' a a f (refl_equal a)) as q.
103 apply inj_pairT2 in H2.
104 apply inj_pairT2 in H1.
110 apply inj_pairT2 in H2.
111 apply inj_pairT2 in H1.
115 Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
116 refine {| fmor := fun a b f => M1 f |}.
122 set (invert_ga _ f') as q.
129 destruct f'; simpl in *.
141 apply (if_associativity
142 ((ga_functor g0 >>>> HomFunctor s0 (enr_c_i s0))) (ga_functor g) (HomFunctor s2 (enr_c_i s2))).
145 Definition M2 (c1 c2 : SMMEs) :
146 (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
147 (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
149 destruct RE; [ apply gaoi_id | idtac ].
151 apply (garrow_from_reification s1 (smme_mee s2) s2 r).
154 Lemma eqv1 a b (f : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)
155 (f' : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)
156 (H : generalizedArrowOrIdentityFunc a b f ≃ generalizedArrowOrIdentityFunc a b f') :
157 generalizedArrowOrIdentityFunc a b (M2 a b (M1 f)) ≃ generalizedArrowOrIdentityFunc a b f'.
159 set (@roundtrip_garrow_to_garrow a b (smme_mee b) (smme_mon b)) as q.
160 destruct f; simpl in *.
163 apply (if_comp (if_inv H)).
167 (garrow_functor s1 (smme_mee s2) s2 (reification_from_garrow s1 s2 g))
168 (HomFunctor (senr_c s2) (senr_c_i s2))
169 (HomFunctor (senr_c s2) (senr_c_i s2))
175 Lemma eqv2 a b (f : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
176 (f' : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
177 (H : reificationOrIdentityFunc a b f ≃ reificationOrIdentityFunc a b f') :
178 reificationOrIdentityFunc _ _ (M1 (M2 _ _ f)) ≃ reificationOrIdentityFunc _ _ f'.
180 set (@roundtrip_reification_to_reification a b (smme_mee b) (smme_mon b)) as q.
184 apply (if_comp (if_inv H)).
193 forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
195 M2 a b f ~~ M2 a b f'.
201 set (invert_reif _ f') as q.
208 unfold garrow_functor.
209 unfold step2_functor.
213 apply (step1_niso smme (smme_mee smme) (smme_mon smme) x).
217 apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
220 apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
221 ff_functor_section_functor me_homfunctor me_full me_faithful))
222 (HomFunctor (senr_c smme) (senr_c_i smme))).
223 apply (if_respects (RestrictToImage x) (RestrictToImage x)).
224 apply (if_id (RestrictToImage x)).
227 apply (if_associativity (R' smme smme x) (ff_functor_section_functor me_homfunctor me_full me_faithful)
228 (HomFunctor (senr_c smme) (senr_c_i smme))).
229 set (roundtrip_lemma (me_full(MonicEnrichment:=smme_mee smme))) as q.
230 set (R' smme smme x) as f.
231 set (me_faithful(MonicEnrichment:=smme_mee smme)) as ff.
232 unfold HomFunctor_fullimage in f.
234 set (q ff _ _ (FullImage x) _ f) as q'.
235 unfold me_homfunctor in q'.
239 destruct f'; simpl in *.
242 eapply if_comp; [ idtac | eapply if_inv; apply H ].
244 unfold garrow_functor.
245 unfold step2_functor.
248 apply (step1_niso smme (smme_mee smme) (smme_mon smme) r).
253 apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
254 ff_functor_section_functor me_homfunctor me_full me_faithful))
255 (HomFunctor (senr_c smme) (senr_c_i smme))).
258 apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
259 apply (if_respects (RestrictToImage x) (RestrictToImage x)).
260 apply (if_id (RestrictToImage x)).
266 apply (if_associativity (R' smme smme x) (ff_functor_section_functor me_homfunctor me_full me_faithful)
267 (HomFunctor (senr_c smme) (senr_c_i smme))).
268 set (roundtrip_lemma (me_full(MonicEnrichment:=smme_mee smme))) as q.
269 set (R' smme smme x) as f.
270 set (me_faithful(MonicEnrichment:=smme_mee smme)) as ff.
271 unfold HomFunctor_fullimage in f.
273 set (q ff _ _ (FullImage x) _ f) as q'.
274 unfold me_homfunctor in q'.
278 unfold garrow_functor.
279 unfold step2_functor.
280 set (step1_niso s1 (smme_mee s2) s2 r) as q.
283 eapply if_comp; [ idtac | apply q ].
286 apply (if_associativity
288 (R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful)
289 (HomFunctor (senr_c s2) (senr_c_i s2))).
292 apply (if_associativity
295 (FullImage_InclusionFunctor _)).
299 (R' s1 s2 r >>>> FullImage_InclusionFunctor _)
300 (((R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful) >>>>
301 HomFunctor (senr_c s2) (senr_c_i s2)))).
305 apply (if_associativity
307 (ff_functor_section_functor me_homfunctor me_full me_faithful)
308 (HomFunctor (senr_c s2) (senr_c_i s2))).
309 apply roundtrip_lemma.
312 set (step1_niso s1 (smme_mee s2) s2 r0) as q'.
315 eapply if_comp; [ idtac | apply q' ].
317 apply (if_associativity
319 (R' s1 s2 r0 >>>> ff_functor_section_functor me_homfunctor me_full me_faithful)
320 (HomFunctor (senr_c s2) (senr_c_i s2))).
323 apply (if_associativity
326 (FullImage_InclusionFunctor _)).
330 (R' s1 s2 r0 >>>> FullImage_InclusionFunctor _)
331 (((R' s1 s2 r0 >>>> ff_functor_section_functor me_homfunctor me_full me_faithful) >>>>
332 HomFunctor (senr_c s2) (senr_c_i s2)))).
336 apply (if_associativity
338 (ff_functor_section_functor me_homfunctor me_full me_faithful)
339 (HomFunctor (senr_c s2) (senr_c_i s2))).
340 apply roundtrip_lemma.
345 Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
346 refine {| fmor := fun a b f => M2 _ _ f |}.
348 intros; simpl; apply if_id.
349 intros; apply (@bijection_lemma _ _ _ _ _ M1_Functor M2); intros.
350 apply M2_respects; auto.
352 apply (@eqv1 _ _ f0 f0).
355 apply (@eqv2 _ _ f0 f0).
359 Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
360 refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
361 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
362 apply (eqv1 _ _ f f'); auto.
363 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
364 apply (eqv2 _ _ f f'); auto.
367 End ReificationsIsomorphicToGeneralizedArrows.