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 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 ReificationCategory.
31 Require Import ReificationsAndGeneralizedArrows.
32 Require Import WeakFunctorCategory.
33 Require Import BijectionLemma.
35 Section ReificationsIsomorphicToGeneralizedArrows.
37 Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
38 (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
39 (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
41 destruct GA; [ apply roi_id | idtac ].
43 apply reification_from_garrow.
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 (mon_i s0))) (ga_functor g) (HomFunctor s2 (me_i s2))).
145 Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
146 (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
147 (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
149 destruct RE; [ apply gaoi_id | idtac ].
151 apply (garrow_from_reification s1 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) as q.
160 destruct f; simpl in *.
163 apply (if_comp (if_inv H)).
166 apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
167 (G0:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor s2 (mon_i s2))).
173 Lemma eqv2 a b (f : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
174 (f' : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
175 (H : reificationOrIdentityFunc a b f ≃ reificationOrIdentityFunc a b f') :
176 reificationOrIdentityFunc _ _ (M1 (M2 _ _ f)) ≃ reificationOrIdentityFunc _ _ f'.
178 set (@roundtrip_reification_to_reification _ a _ _ b) as q.
182 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.
207 unfold garrow_functor.
208 unfold step2_functor.
211 apply (if_comp (@step1_niso _ smme _ _ smme x)).
213 apply (@roundtrip_lemma _ smme _ _ smme x).
215 destruct f'; simpl in *.
220 unfold garrow_functor.
221 unfold step2_functor.
222 apply (if_comp (@step1_niso _ smme _ _ smme r)).
224 apply (@roundtrip_lemma _ smme _ _ smme r).
226 unfold garrow_functor.
227 unfold step2_functor.
229 apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
231 apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
232 apply (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) (if_comp H (@step1_niso _ s1 _ _ s2 r))).
235 Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
236 refine {| fmor := fun a b f => M2 _ _ f |}.
238 intros; simpl; apply if_id.
239 intros; apply (@bijection_lemma _ _ _ _ _ M1_Functor M2); intros.
240 apply M2_respects; auto.
242 apply (@eqv1 _ _ f0 f0).
245 apply (@eqv2 _ _ f0 f0).
249 Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
250 refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
251 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
252 apply (eqv1 _ _ f f'); auto.
253 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
254 apply (eqv2 _ _ f f'); auto.
257 End ReificationsIsomorphicToGeneralizedArrows.