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).
215 set (roundtrip_lemma smme (smme_mee smme) (smme_mon smme) x) as q.
218 apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
221 apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
222 ff_functor_section_functor me_homfunctor me_full me_faithful))
223 (HomFunctor (senr_c smme) (senr_c_i smme))).
224 apply (if_respects (RestrictToImage x) (RestrictToImage x)).
225 apply (if_id (RestrictToImage x)).
227 unfold me_homfunctor in q.
232 destruct f'; simpl in *.
235 eapply if_comp; [ idtac | eapply if_inv; apply H ].
237 unfold garrow_functor.
238 unfold step2_functor.
241 apply (step1_niso smme (smme_mee smme) (smme_mon smme) r).
246 apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
247 ff_functor_section_functor me_homfunctor me_full me_faithful))
248 (HomFunctor (senr_c smme) (senr_c_i smme))).
251 apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
252 apply (if_respects (RestrictToImage x) (RestrictToImage x)).
253 apply (if_id (RestrictToImage x)).
256 set (roundtrip_lemma smme (smme_mee smme) (smme_mon smme) x) as q.
258 unfold me_homfunctor in q.
263 unfold garrow_functor.
264 unfold step2_functor.
265 set (step1_niso s1 (smme_mee s2) s2 r) as q.
268 eapply if_comp; [ idtac | apply q ].
271 apply (if_associativity
273 (R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful)
274 (HomFunctor (senr_c s2) (senr_c_i s2))).
277 apply (if_associativity
280 (FullImage_InclusionFunctor _)).
284 (R' s1 s2 r >>>> FullImage_InclusionFunctor _)
285 (((R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful) >>>>
286 HomFunctor (senr_c s2) (senr_c_i s2)))).
290 apply (if_associativity
292 (ff_functor_section_functor me_homfunctor me_full me_faithful)
293 (HomFunctor (senr_c s2) (senr_c_i s2))).
298 (FullImage_InclusionFunctor _)
299 ((ff_functor_section_functor me_homfunctor me_full me_faithful >>>> HomFunctor _ _))
303 apply (RestrictToImage_splits_niso (HomFunctor s2 (senr_c_i s2))).
306 Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
307 refine {| fmor := fun a b f => M2 _ _ f |}.
309 intros; simpl; apply if_id.
310 intros; apply (@bijection_lemma _ _ _ _ _ M1_Functor M2); intros.
311 apply M2_respects; auto.
313 apply (@eqv1 _ _ f0 f0).
316 apply (@eqv2 _ _ f0 f0).
320 Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
321 refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
322 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
323 apply (eqv1 _ _ f f'); auto.
324 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
325 apply (eqv2 _ _ f f'); auto.
328 End ReificationsIsomorphicToGeneralizedArrows.