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.
31 Section ReificationsEquivalentToGeneralizedArrows.
34 match goal with [ |- ?A ≃ ?B ] => refine (@if_comp _ _ _ _ _ _ _ A _ _ _ B _ _)
37 Lemma roundtrip_lemma'
38 `{C:Category}`{D:Category}`{E:Category}
39 {Gobj}(G:Functor E D Gobj) G_full G_faithful {Fobj}(F:Functor C (FullImage G) Fobj) :
40 ((F >>>> ff_functor_section_functor G G_full G_faithful) >>>> G) ≃ (F >>>> InclusionFunctor _ _).
42 apply (if_associativity F (ff_functor_section_functor G _ _) G).
45 if_transitive; [ idtac | apply if_left_identity ].
46 apply (if_comp(F2:=(ff_functor_section_functor G G_full G_faithful) >>>> RestrictToImage G >>>> InclusionFunctor _ _)).
48 apply (if_associativity (ff_functor_section_functor G G_full G_faithful) (RestrictToImage G) (InclusionFunctor D (FullImage G))).
50 apply ff_functor_section_splits_niso.
54 Definition roundtrip_lemma
55 `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
56 := roundtrip_lemma' (RepresentableFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification).
58 Lemma roundtrip_reification_to_reification
59 `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
60 : reification ≃ reification_from_garrow K C (garrow_from_reification K C reification).
63 unfold garrow_functor.
64 apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).
65 apply (@step1_niso _ K _ _ C reification).
66 apply (if_inv (roundtrip_lemma K C reification)).
69 Lemma roundtrip_garrow_to_garrow
70 `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (garrow : GeneralizedArrow K C)
71 : garrow ≃ garrow_from_reification K C (reification_from_garrow K C garrow).
72 apply (ffc_functor_weakly_monic _ (ffme_mf_conservative C)).
74 apply (if_comp(F2:=(step1_functor K C (reification_from_garrow K C garrow)
75 >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).
77 unfold garrow_from_reification.
78 unfold garrow_functor.
80 set (@roundtrip_lemma _ K _ _ C) as q.
81 apply (q (reification_from_garrow K C garrow)).
83 apply (step1_niso K C (reification_from_garrow K C garrow)).
86 End ReificationsEquivalentToGeneralizedArrows.