src/ReificationsAndGeneralizedArrows.v

   1 (*********************************************************************************************************************************)
   2 (* ReificationsAndGeneralizedArrows:                                                                                             *)
   3 (*                                                                                                                               *)
   4 (*   For each pair of enrichments E1 and E2, there is a bijection between the generalized arrows E1->E2 and the reifications     *)
   5 (*   E1->E2                                                                                                                      *)
   6 (*                                                                                                                               *)
   7 (*********************************************************************************************************************************)
   8
   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.
  33
  34 Section ReificationsEquivalentToGeneralizedArrows.
  35
  36   Ltac if_transitive :=
  37     match goal with [ |- ?A ≃ ?B ] => refine (@if_comp _ _ _ _ _ _ _ A _ _ _ B _ _)
  38     end.
  39
  40   Lemma roundtrip_lemma
  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 _).
  44     if_transitive.
  45       eapply if_inv.
  46       apply (if_associativity F (ff_functor_section_functor G _ _) G).
  47     if_transitive.
  48       apply (if_associativity F (ff_functor_section_functor G _ _) G).
  49       apply if_respects.
  50         apply if_id.
  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 _)).
  53     apply if_inv.
  54     apply (if_associativity (ff_functor_section_functor G G_full G_faithful)
  55       (RestrictToImage G) (FullImage_InclusionFunctor G)).
  56     apply if_respects.
  57     apply ff_functor_section_splits_niso.
  58     apply if_id.
  59     Qed.
  60
  61   Definition step1_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).
  65     intros.
  66     simpl.
  67     etransitivity.
  68     eapply comp_respects; [ apply reflexivity | idtac ].
  69     apply associativity.
  70     apply iso_comp1_right.
  71     Qed.
  72
  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).
  76     apply if_inv.
  77     eapply if_comp.
  78     eapply if_inv.
  79     unfold garrow_from_reification.
  80     simpl.
  81     unfold mf_F.
  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))
  86       (step2_functor C)).
  87
  88     apply (ffc_functor_weakly_monic _ me_full me_faithful me_conservative me_conservative).
  89     eapply if_comp.
  90     apply (if_associativity
  91       (RestrictToImage (reification_from_garrow K CM garrow) >>>> R' K CM (reification_from_garrow K CM garrow))
  92       (step2_functor C)
  93       me_homfunctor).
  94
  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'.
  99
 100     eapply if_comp.
 101       apply (if_associativity (RestrictToImage (reification_from_garrow K CM garrow)) f (step2_functor C >>>> me_homfunctor)).
 102       unfold step2_functor.
 103       eapply if_comp.
 104       apply (if_respects
 105         (RestrictToImage (reification_from_garrow K CM garrow))
 106         (RestrictToImage (reification_from_garrow K CM garrow))
 107         _ _ (if_id _) q').
 108
 109     eapply if_comp.
 110       eapply if_inv.
 111       apply (if_associativity (RestrictToImage (reification_from_garrow K CM garrow)) f (FullImage_InclusionFunctor me_homfunctor)).
 112
 113     apply if_inv.
 114       apply (step1_niso K C CM (reification_from_garrow K CM garrow)).
 115       Qed.
 116
 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).
 120
 121     simpl.
 122       unfold garrow_functor.
 123
 124     eapply if_comp.
 125       apply (step1_niso K C CM reification).
 126
 127     unfold garrow_monoidal.
 128       unfold mf_F.
 129       apply if_inv.
 130       eapply if_comp.
 131       apply (if_associativity (RestrictToImage reification) (R' K CM reification >>>> step2_functor C)
 132         (HomFunctor ce (pmon_I (enr_c_pm ce)))).
 133       apply if_inv.
 134       eapply if_comp.
 135       apply (if_associativity (RestrictToImage reification) (R' K CM reification)
 136         (FullImage_InclusionFunctor (HomFunctor ce (pmon_I (enr_c_pm ce))))).
 137
 138     apply (if_respects (RestrictToImage reification) (RestrictToImage reification) _ _ (if_id _)).
 139       apply if_inv.
 140       eapply if_comp.
 141       apply (if_associativity  (R' K CM reification) (step2_functor C) (HomFunctor ce _)).
 142
 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'.
 147       apply q'.
 148       Qed.
 149
 150 End ReificationsEquivalentToGeneralizedArrows.