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 PreMonoidalCategories.
23 Require Import Coherence_ch7_8.
24 Require Import Enrichment_ch2_8.
25 Require Import Enrichments.
26 Require Import RepresentableStructure_ch7_2.
27 Require Import Reification.
28 Require Import GeneralizedArrow.
29 Require Import GeneralizedArrowFromReification.
30 Require Import ReificationFromGeneralizedArrow.
31 Require Import ReificationCategory.
32 Require Import GeneralizedArrowCategory.
34 Section ReificationsEquivalentToGeneralizedArrows.
37 match goal with [ |- ?A ≃ ?B ] => refine (@if_comp _ _ _ _ _ _ _ A _ _ _ B _ _)
41 `{D:Category}`{E:Category}
42 {Gobj}{G:Functor E D Gobj} G_full G_faithful `{C:Category}{Fobj}(F:Functor C (FullImage G) Fobj) :
43 (F >>>> (ff_functor_section_functor G G_full G_faithful >>>> G)) ≃ (F >>>> FullImage_InclusionFunctor _).
46 apply (if_associativity F (ff_functor_section_functor G _ _) G).
48 apply (if_associativity F (ff_functor_section_functor G _ _) G).
51 if_transitive; [ idtac | apply if_left_identity ].
52 apply (if_comp(F2:=(ff_functor_section_functor G G_full G_faithful) >>>> RestrictToImage G >>>> FullImage_InclusionFunctor _)).
54 apply (if_associativity (ff_functor_section_functor G G_full G_faithful)
55 (RestrictToImage G) (FullImage_InclusionFunctor G)).
57 apply ff_functor_section_splits_niso.
62 `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (reification : Reification K ce (enr_c_i ce))
63 : reification_rstar reification ≃ (RestrictToImage reification >>>> R' K CM reification >>>> FullImage_InclusionFunctor CM).
64 exists (fun c1 => homset_tensor_iso K CM reification c1).
68 eapply comp_respects; [ apply reflexivity | idtac ].
70 apply iso_comp1_right.
73 Lemma roundtrip_garrow_to_garrow
74 `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (garrow : GeneralizedArrow K ce)
75 : garrow ≃ garrow_from_reification K C CM (reification_from_garrow K CM garrow).
79 unfold garrow_from_reification.
82 unfold garrow_functor.
83 apply (if_associativity
84 (RestrictToImage (reification_from_garrow K CM garrow))
85 (R' K CM (reification_from_garrow K CM garrow))
88 apply (ffc_functor_weakly_monic _ me_full me_faithful me_conservative me_conservative).
90 apply (if_associativity
91 (RestrictToImage (reification_from_garrow K CM garrow) >>>> R' K CM (reification_from_garrow K CM garrow))
95 set ((R' K CM (reification_from_garrow K CM garrow))) as f.
96 unfold HomFunctor_fullimage in f.
97 set (roundtrip_lemma (me_full(MonicEnrichment:=C))) as q.
98 set (q (me_faithful(MonicEnrichment:=C)) _ _ _ _ f) as q'.
101 apply (if_associativity (RestrictToImage (reification_from_garrow K CM garrow)) f (step2_functor C >>>> me_homfunctor)).
102 unfold step2_functor.
105 (RestrictToImage (reification_from_garrow K CM garrow))
106 (RestrictToImage (reification_from_garrow K CM garrow))
111 apply (if_associativity (RestrictToImage (reification_from_garrow K CM garrow)) f (FullImage_InclusionFunctor me_homfunctor)).
114 apply (step1_niso K C CM (reification_from_garrow K CM garrow)).
117 Lemma roundtrip_reification_to_reification
118 `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (reification : Reification K ce (enr_c_i ce))
119 : reification ≃ reification_from_garrow K CM (garrow_from_reification K C CM reification).
122 unfold garrow_functor.
125 apply (step1_niso K C CM reification).
127 unfold garrow_monoidal.
131 apply (if_associativity (RestrictToImage reification) (R' K CM reification >>>> step2_functor C)
132 (HomFunctor ce (pmon_I (enr_c_pm ce)))).
135 apply (if_associativity (RestrictToImage reification) (R' K CM reification)
136 (FullImage_InclusionFunctor (HomFunctor ce (pmon_I (enr_c_pm ce))))).
138 apply (if_respects (RestrictToImage reification) (RestrictToImage reification) _ _ (if_id _)).
141 apply (if_associativity (R' K CM reification) (step2_functor C) (HomFunctor ce _)).
143 set ((R' K CM reification)) as f.
144 unfold HomFunctor_fullimage in f.
145 set (roundtrip_lemma (me_full(MonicEnrichment:=C))) as q.
146 set (q (me_faithful(MonicEnrichment:=C)) _ _ _ _ f) as q'.
150 End ReificationsEquivalentToGeneralizedArrows.