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 CM)
  75     : garrow ≃ garrow_from_reification K C CM (reification_from_garrow K CM garrow).
  76
  77     apply if_inv.
  78     eapply if_comp.
  79     eapply if_inv.
  80     unfold garrow_from_reification.
  81     simpl.
  82     unfold mf_F.
  83     unfold garrow_functor.
  84     apply (if_associativity
  85       (RestrictToImage (reification_from_garrow K CM garrow))
  86       (R' K CM (reification_from_garrow K CM garrow))
  87       (step2_functor C)).
  88
  89     apply (ffc_functor_weakly_monic _ me_full me_faithful me_conservative me_conservative).
  90     eapply if_comp.
  91     apply (if_associativity
  92       (RestrictToImage (reification_from_garrow K CM garrow) >>>> R' K CM (reification_from_garrow K CM garrow))
  93       (step2_functor C)
  94       me_homfunctor).
  95
  96     set ((R' K CM (reification_from_garrow K CM garrow))) as f.
  97     unfold HomFunctor_fullimage in f.
  98     set (roundtrip_lemma (me_full(MonicEnrichment:=C))) as q.
  99     set (q (me_faithful(MonicEnrichment:=C)) _ _ _ _ f) as q'.
 100
 101     eapply if_comp.
 102       apply (if_associativity (RestrictToImage (reification_from_garrow K CM garrow)) f (step2_functor C >>>> me_homfunctor)).
 103       unfold step2_functor.
 104       eapply if_comp.
 105       apply (if_respects
 106         (RestrictToImage (reification_from_garrow K CM garrow))
 107         (RestrictToImage (reification_from_garrow K CM garrow))
 108         _ _ (if_id _) q').
 109
 110     eapply if_comp.
 111       eapply if_inv.
 112       apply (if_associativity (RestrictToImage (reification_from_garrow K CM garrow)) f (FullImage_InclusionFunctor me_homfunctor)).
 113
 114     apply if_inv.
 115       apply (step1_niso K C CM (reification_from_garrow K CM garrow)).
 116       Qed.
 117
 118   Lemma roundtrip_reification_to_reification
 119     `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (reification : Reification K ce (enr_c_i ce))
 120     : reification ≃ reification_from_garrow K CM (garrow_from_reification K C CM reification).
 121
 122     simpl.
 123       unfold garrow_functor.
 124
 125     eapply if_comp.
 126       apply (step1_niso K C CM reification).
 127
 128     unfold garrow_monoidal.
 129       unfold mf_F.
 130       apply if_inv.
 131       eapply if_comp.
 132       apply (if_associativity (RestrictToImage reification) (R' K CM reification >>>> step2_functor C)
 133         (HomFunctor ce (pmon_I (enr_c_pm ce)))).
 134       apply if_inv.
 135       eapply if_comp.
 136       apply (if_associativity (RestrictToImage reification) (R' K CM reification)
 137         (FullImage_InclusionFunctor (HomFunctor ce (pmon_I (enr_c_pm ce))))).
 138
 139     apply (if_respects (RestrictToImage reification) (RestrictToImage reification) _ _ (if_id _)).
 140       apply if_inv.
 141       eapply if_comp.
 142       apply (if_associativity  (R' K CM reification) (step2_functor C) (HomFunctor ce _)).
 143
 144     set ((R' K CM reification)) as f.
 145       unfold HomFunctor_fullimage in f.
 146       set (roundtrip_lemma (me_full(MonicEnrichment:=C))) as q.
 147       set (q (me_faithful(MonicEnrichment:=C)) _ _ _ _ f) as q'.
 148       apply q'.
 149       Qed.
 150
 151 End ReificationsEquivalentToGeneralizedArrows.