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.
34 Section ReificationsIsomorphicToGeneralizedArrows.
37 Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) :
39 garrow_fobj' s1 s2 r12 (ehom(ECategory:=s1) (me_i s1) (garrow_fobj s0 s1 r01 A))
40 ≅ garrow_fobj' s0 s2 (compose_reifications s0 s1 s2 r01 r12) A.
43 Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) :
44 (step1_functor s0 s1 r01 >>>>
45 InclusionFunctor (enr_v s1) (FullImage (RepresentableFunctor s1 (me_i s1)))) >>>> step1_functor s1 s2 r12
46 ≃ step1_functor s0 s2 (compose_reifications s0 s1 s2 r01 r12).
50 Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
51 (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
52 (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
54 destruct GA; [ apply roi_id | idtac ].
56 apply reification_from_garrow.
60 (* I tried really hard to avoid this *)
61 Require Import Coq.Logic.Eqdep.
63 Inductive Heq : forall {A}{B}, A -> B -> Prop :=
64 heq : forall {A} (a:A), Heq a a.
66 Lemma invert_ga' : forall (a b: SMME)
67 (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>b), a=b ->
68 (Heq f (gaoi_id a)) \/ (exists f', Heq f (gaoi_ga a b f')).
77 Lemma invert_ga : forall (a: SMME)
78 (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
79 (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
81 set (invert_ga' a a f (refl_equal a)) as q.
85 apply inj_pairT2 in H2.
86 apply inj_pairT2 in H1.
92 apply inj_pairT2 in H2.
93 apply inj_pairT2 in H1.
97 Lemma invert_reif' : forall (a b: SMME)
98 (f:a~~{MorphismsOfCategoryOfReifications}~~>b), a=b ->
99 (Heq f (roi_id a)) \/ (exists f', Heq f (roi_reif a b f')).
108 Lemma invert_reif : forall (a: SMME)
109 (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
110 (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
112 set (invert_reif' a a f (refl_equal a)) as q.
116 apply inj_pairT2 in H2.
117 apply inj_pairT2 in H1.
123 apply inj_pairT2 in H2.
124 apply inj_pairT2 in H1.
128 Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
129 refine {| fmor := fun a b f => M1 f |}.
135 set (invert_ga _ f') as q.
142 destruct f'; simpl in *.
154 apply (if_associativity
155 ((ga_functor g0 >>>> RepresentableFunctor s0 (mon_i s0))) (ga_functor g) (RepresentableFunctor s2 (me_i s2))).
158 Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
159 (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
160 (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
162 destruct RE; [ apply gaoi_id | idtac ].
164 apply (garrow_from_reification s1 s2 r).
168 forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
170 M2 a b f ~~ M2 a b f'.
176 set (invert_reif _ f') as q.
182 unfold garrow_functor.
183 unfold step2_functor.
186 apply (if_comp (@step1_niso _ smme _ _ smme x)).
188 apply (@roundtrip_lemma _ smme _ _ smme x).
190 destruct f'; simpl in *.
195 unfold garrow_functor.
196 unfold step2_functor.
197 apply (if_comp (@step1_niso _ smme _ _ smme r)).
199 apply (@roundtrip_lemma _ smme _ _ smme r).
201 unfold garrow_functor.
202 unfold step2_functor.
204 set (if_comp H (@step1_niso _ s1 _ _ s2 r)) as yy.
205 set (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) yy) as yy'.
206 apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
208 apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
212 Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
213 refine {| fmor := fun a b f => M2 _ _ f |}.
215 intros; simpl; apply if_id.
224 (F0:=((garrow_functor s1 s0 r >>>> RepresentableFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0))
225 (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0)))
226 (G0:=(RepresentableFunctor s2 (mon_i s2)))
227 (G1:=(RepresentableFunctor s2 (mon_i s2))));
228 [ idtac | apply if_id ].
231 apply (if_associativity (garrow_functor s1 s0 r) (RepresentableFunctor s0 (mon_i s0)) (garrow_functor s0 s2 r0)).
232 Set Printing Coercions.
234 unfold garrow_functor at 1.
235 unfold step2_functor at 1.
236 set (roundtrip_lemma'
237 (RepresentableFunctor (enr_c (smme_e s0)) (me_i (smme_mon s0)))
238 (ffme_mf_full (smme_mee s0)) (ffme_mf_faithful (smme_mee s0))
239 (step1_functor (smme_see s1) (smme_mee s0) r)
242 (G0:=garrow_functor (smme_see s0) (smme_mee s2) r0)
243 (G1:=garrow_functor (smme_see s0) (smme_mee s2) r0)
246 Unset Printing Coercions.
248 unfold garrow_functor at 2.
249 unfold garrow_functor at 1.
252 apply (if_associativity _ (step1_functor s0 s2 r0) (step2_functor s2)).
254 (G0:=step2_functor s2)
255 (G1:=step2_functor s2)); [ idtac | apply if_id ].
259 Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
260 refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
261 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
263 set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
264 destruct f; simpl in *.
267 apply (if_comp (if_inv H)).
270 apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
271 (G0:=RepresentableFunctor s2 (mon_i s2))(G1:=RepresentableFunctor s2 (mon_i s2))).
275 unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
277 set (@roundtrip_reification_to_reification _ a _ _ b) as q.
281 apply (if_comp (if_inv H)).
291 End ReificationsIsomorphicToGeneralizedArrows.