1 (*********************************************************************************************************************************)
2 (* ReificationsAndGeneralizedArrows: *)
4 (* For each pair of enrichments E1 and E2, there is a bijection between the generalized arrows E1->E2 and the reifications *)
7 (*********************************************************************************************************************************)
9 Generalizable All Variables.
10 Require Import Preamble.
11 Require Import General.
12 Require Import Categories_ch1_3.
13 Require Import Functors_ch1_4.
14 Require Import Isomorphisms_ch1_5.
15 Require Import ProductCategories_ch1_6_1.
16 Require Import OppositeCategories_ch1_6_2.
17 Require Import Enrichment_ch2_8.
18 Require Import Subcategories_ch7_1.
19 Require Import NaturalTransformations_ch7_4.
20 Require Import NaturalIsomorphisms_ch7_5.
21 Require Import MonoidalCategories_ch7_8.
22 Require Import Coherence_ch7_8.
23 Require Import Enrichment_ch2_8.
24 Require Import RepresentableStructure_ch7_2.
25 Require Import Reification.
26 Require Import GeneralizedArrow.
27 Require Import GeneralizedArrowFromReification.
28 Require Import ReificationFromGeneralizedArrow.
29 Require Import ReificationCategory.
30 Require Import GeneralizedArrowCategory.
32 Section ReificationsEquivalentToGeneralizedArrows.
35 match goal with [ |- ?A ≃ ?B ] => refine (@if_comp _ _ _ _ _ _ _ A _ _ _ B _ _)
38 Lemma roundtrip_lemma'
39 `{C:Category}`{D:Category}`{E:Category}
40 {Gobj}(G:Functor E D Gobj) G_full G_faithful {Fobj}(F:Functor C (FullImage G) Fobj) :
41 ((F >>>> ff_functor_section_functor G G_full G_faithful) >>>> G) ≃ (F >>>> InclusionFunctor _ _).
43 apply (if_associativity F (ff_functor_section_functor G _ _) G).
46 if_transitive; [ idtac | apply if_left_identity ].
47 apply (if_comp(F2:=(ff_functor_section_functor G G_full G_faithful) >>>> RestrictToImage G >>>> InclusionFunctor _ _)).
49 apply (if_associativity (ff_functor_section_functor G G_full G_faithful) (RestrictToImage G) (InclusionFunctor D (FullImage G))).
51 apply ff_functor_section_splits_niso.
55 Definition roundtrip_lemma
56 `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
57 := roundtrip_lemma' (HomFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification).
59 Lemma roundtrip_reification_to_reification
60 `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
61 : reification ≃ reification_from_garrow K C (garrow_from_reification K C reification).
64 unfold garrow_functor.
65 apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))).
66 apply (@step1_niso _ K _ _ C reification).
67 apply (if_inv (roundtrip_lemma K C reification)).
70 Lemma roundtrip_garrow_to_garrow
71 `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (garrow : GeneralizedArrow K C)
72 : garrow ≃ garrow_from_reification K C (reification_from_garrow K C garrow).
73 apply (ffc_functor_weakly_monic _ (ffme_mf_full C) (ffme_mf_faithful C) (ffme_mf_conservative C) (ffme_mf_conservative C)).
75 apply (if_comp(F2:=(step1_functor K C (reification_from_garrow K C garrow)
76 >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))).
78 unfold garrow_from_reification.
79 unfold garrow_functor.
81 set (@roundtrip_lemma _ K _ _ C) as q.
82 apply (q (reification_from_garrow K C garrow)).
84 apply (step1_niso K C (reification_from_garrow K C garrow)).
87 End ReificationsEquivalentToGeneralizedArrows.