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.
35 Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
36 (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
37 (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
39 destruct GA; [ apply roi_id | idtac ].
41 apply reification_from_garrow.
45 Lemma invert_ga : forall (a: SMME)
46 (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
47 (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
51 Lemma invert_reif : forall (a: SMME)
52 (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
53 (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
57 Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
58 refine {| fmor := fun a b f => M1 f |}.
64 set (invert_ga _ f') as q.
71 destruct f'; simpl in *.
83 apply (if_associativity
84 ((ga_functor g0 >>>> RepresentableFunctor s0 (mon_i s0))) (ga_functor g) (RepresentableFunctor s2 (me_i s2))).
87 Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
88 (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
89 (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
91 destruct RE; [ apply gaoi_id | idtac ].
93 apply (garrow_from_reification s1 s2 r).
97 forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
99 M2 a b f ~~ M2 a b f'.
105 set (invert_reif _ f') as q.
111 unfold garrow_functor.
112 unfold step2_functor.
115 apply (if_comp (@step1_niso _ smme _ _ smme x)).
117 apply (@roundtrip_lemma _ smme _ _ smme x).
119 destruct f'; simpl in *.
124 unfold garrow_functor.
125 unfold step2_functor.
126 apply (if_comp (@step1_niso _ smme _ _ smme r)).
128 apply (@roundtrip_lemma _ smme _ _ smme r).
130 unfold garrow_functor.
131 unfold step2_functor.
133 set (if_comp H (@step1_niso _ s1 _ _ s2 r)) as yy.
134 set (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) yy) as yy'.
135 apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
137 apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
141 Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
142 refine {| fmor := fun a b f => M2 _ _ f |}.
144 intros; simpl; apply if_id.
153 (F0:=((garrow_functor s1 s0 r >>>> RepresentableFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0))
154 (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0)))
155 (G0:=(RepresentableFunctor s2 (mon_i s2)))
156 (G1:=(RepresentableFunctor s2 (mon_i s2))));
157 [ idtac | apply if_id ].
161 Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
162 refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
163 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
165 set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
166 destruct f; simpl in *.
169 apply (if_comp (if_inv H)).
172 apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
173 (G0:=RepresentableFunctor s2 (mon_i s2))(G1:=RepresentableFunctor s2 (mon_i s2))).
177 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
179 set (@roundtrip_reification_to_reification _ a _ _ b) as q.
183 apply (if_comp (if_inv H)).
193 End ReificationsIsomorphicToGeneralizedArrows.