1 (*********************************************************************************************************************************)
2 (* ReificationsEquivalentToGeneralizedArrows: *)
4 (* The category of generalized arrows and the category of reifications are equivalent 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 MonoidalCategories_ch7_8.
21 Require Import Coherence_ch7_8.
22 Require Import Enrichment_ch2_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 ReificationsEquivalentToGeneralizedArrows.
31 Require Import WeakFunctorCategory.
33 Section ReificationsIsomorphicToGeneralizedArrows.
36 Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) :
38 garrow_fobj' s1 s2 r12 (ehom(ECategory:=s1) (me_i s1) (garrow_fobj s0 s1 r01 A))
39 ≅ garrow_fobj' s0 s2 (compose_reifications s0 s1 s2 r01 r12) A.
42 Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) :
43 (step1_functor s0 s1 r01 >>>>
44 InclusionFunctor (enr_v s1) (FullImage (RepresentableFunctor s1 (me_i s1)))) >>>> step1_functor s1 s2 r12
45 ≃ step1_functor s0 s2 (compose_reifications s0 s1 s2 r01 r12).
46 unfold IsomorphicFunctors.
49 unfold compose_reifications at 0.
50 eapply Build_IsomorphicFunctors.
52 unfold InclusionFunctor.
59 Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
60 (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
61 (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
63 destruct GA; [ apply roi_id | idtac ].
65 apply reification_from_garrow.
69 (* I tried really hard to avoid this *)
70 Require Import Coq.Logic.Eqdep.
72 Inductive Heq : forall {A}{B}, A -> B -> Prop :=
73 heq : forall {A} (a:A), Heq a a.
75 Lemma invert_ga' : forall (a b: SMME)
76 (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>b), a=b ->
77 (Heq f (gaoi_id a)) \/ (exists f', Heq f (gaoi_ga a b f')).
86 Lemma invert_ga : forall (a: SMME)
87 (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
88 (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
90 set (invert_ga' a a f (refl_equal a)) as q.
94 apply inj_pairT2 in H2.
95 apply inj_pairT2 in H1.
101 apply inj_pairT2 in H2.
102 apply inj_pairT2 in H1.
106 Lemma invert_reif' : forall (a b: SMME)
107 (f:a~~{MorphismsOfCategoryOfReifications}~~>b), a=b ->
108 (Heq f (roi_id a)) \/ (exists f', Heq f (roi_reif a b f')).
117 Lemma invert_reif : forall (a: SMME)
118 (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
119 (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
121 set (invert_reif' a a f (refl_equal a)) as q.
125 apply inj_pairT2 in H2.
126 apply inj_pairT2 in H1.
132 apply inj_pairT2 in H2.
133 apply inj_pairT2 in H1.
137 Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
138 refine {| fmor := fun a b f => M1 f |}.
144 set (invert_ga _ f') as q.
151 destruct f'; simpl in *.
163 apply (if_associativity
164 ((ga_functor g0 >>>> RepresentableFunctor s0 (mon_i s0))) (ga_functor g) (RepresentableFunctor s2 (me_i s2))).
167 Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
168 (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
169 (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
171 destruct RE; [ apply gaoi_id | idtac ].
173 apply (garrow_from_reification s1 s2 r).
177 forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
179 M2 a b f ~~ M2 a b f'.
185 set (invert_reif _ f') as q.
191 unfold garrow_functor.
192 unfold step2_functor.
195 apply (if_comp (@step1_niso _ smme _ _ smme x)).
197 apply (@roundtrip_lemma _ smme _ _ smme x).
199 destruct f'; simpl in *.
204 unfold garrow_functor.
205 unfold step2_functor.
206 apply (if_comp (@step1_niso _ smme _ _ smme r)).
208 apply (@roundtrip_lemma _ smme _ _ smme r).
210 unfold garrow_functor.
211 unfold step2_functor.
213 set (if_comp H (@step1_niso _ s1 _ _ s2 r)) as yy.
214 set (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) yy) as yy'.
215 apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
217 apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
221 Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
222 refine {| fmor := fun a b f => M2 _ _ f |}.
224 intros; simpl; apply if_id.
233 (F0:=((garrow_functor s1 s0 r >>>> RepresentableFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0))
234 (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0)))
235 (G0:=(RepresentableFunctor s2 (mon_i s2)))
236 (G1:=(RepresentableFunctor s2 (mon_i s2))));
237 [ idtac | apply if_id ].
240 apply (if_associativity (garrow_functor s1 s0 r) (RepresentableFunctor s0 (mon_i s0)) (garrow_functor s0 s2 r0)).
241 Set Printing Coercions.
243 unfold garrow_functor at 1.
244 unfold step2_functor at 1.
245 set (roundtrip_lemma'
246 (RepresentableFunctor (enr_c (smme_e s0)) (me_i (smme_mon s0)))
247 (ffme_mf_full (smme_mee s0)) (ffme_mf_faithful (smme_mee s0))
248 (step1_functor (smme_see s1) (smme_mee s0) r)
251 (G0:=garrow_functor (smme_see s0) (smme_mee s2) r0)
252 (G1:=garrow_functor (smme_see s0) (smme_mee s2) r0)
255 Unset Printing Coercions.
257 unfold garrow_functor at 2.
258 unfold garrow_functor at 1.
261 apply (if_associativity _ (step1_functor s0 s2 r0) (step2_functor s2)).
263 (G0:=step2_functor s2)
264 (G1:=step2_functor s2)); [ idtac | apply if_id ].
268 Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
269 refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
270 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
272 set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
273 destruct f; simpl in *.
276 apply (if_comp (if_inv H)).
279 apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
280 (G0:=RepresentableFunctor s2 (mon_i s2))(G1:=RepresentableFunctor s2 (mon_i s2))).
284 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
286 set (@roundtrip_reification_to_reification _ a _ _ b) as q.
290 apply (if_comp (if_inv H)).
300 End ReificationsIsomorphicToGeneralizedArrows.