X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsAndGeneralizedArrows.v;h=4056c779052ba2fd53fd93df63bfb12439b56850;hp=6a615aca9effe6da6c4ede86ebd3c3fbddb0386b;hb=64d416692bda1d36c33b5efa245d46dcf546ad4a;hpb=562e94b529f34fb3854be7914a49190c5243c55a

diff --git a/src/ReificationsAndGeneralizedArrows.v b/src/ReificationsAndGeneralizedArrows.v
index 6a615ac..4056c77 100644
--- a/src/ReificationsAndGeneralizedArrows.v
+++ b/src/ReificationsAndGeneralizedArrows.v
@@ -19,8 +19,10 @@ Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
 Require Import MonoidalCategories_ch7_8.
+Require Import PreMonoidalCategories.
 Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
+Require Import Enrichments.
 Require Import RepresentableStructure_ch7_2.
 Require Import Reification.
 Require Import GeneralizedArrow.
@@ -35,53 +37,115 @@ Section ReificationsEquivalentToGeneralizedArrows.
     match goal with [ |- ?A ≃ ?B ] => refine (@if_comp _ _ _ _ _ _ _ A _ _ _ B _ _)
     end.
 
-  Lemma roundtrip_lemma'
-    `{C:Category}`{D:Category}`{E:Category}
-    {Gobj}(G:Functor E D Gobj) G_full G_faithful {Fobj}(F:Functor C (FullImage G) Fobj) :
-    ((F >>>> ff_functor_section_functor G G_full G_faithful) >>>> G) ≃ (F >>>> InclusionFunctor _ _).
+  Lemma roundtrip_lemma
+    `{D:Category}`{E:Category}
+    {Gobj}{G:Functor E D Gobj} G_full G_faithful `{C:Category}{Fobj}(F:Functor C (FullImage G) Fobj) :
+    (F >>>> (ff_functor_section_functor G G_full G_faithful >>>> G)) ≃ (F >>>> FullImage_InclusionFunctor _).
+    if_transitive.
+      eapply if_inv.
+      apply (if_associativity F (ff_functor_section_functor G _ _) G).
     if_transitive.
       apply (if_associativity F (ff_functor_section_functor G _ _) G).
       apply if_respects.
         apply if_id.
         if_transitive; [ idtac | apply if_left_identity ].
-    apply (if_comp(F2:=(ff_functor_section_functor G G_full G_faithful) >>>> RestrictToImage G >>>> InclusionFunctor _ _)).
+    apply (if_comp(F2:=(ff_functor_section_functor G G_full G_faithful) >>>> RestrictToImage G >>>> FullImage_InclusionFunctor _)).
     apply if_inv.
-    apply (if_associativity (ff_functor_section_functor G G_full G_faithful) (RestrictToImage G) (InclusionFunctor D (FullImage G))).
+    apply (if_associativity (ff_functor_section_functor G G_full G_faithful)
+      (RestrictToImage G) (FullImage_InclusionFunctor G)).
     apply if_respects.
     apply ff_functor_section_splits_niso.
     apply if_id.
     Qed.
 
-  Definition roundtrip_lemma
-    `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
-    := roundtrip_lemma' (HomFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification).
-
-  Lemma roundtrip_reification_to_reification
-    `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
-    : reification ≃ reification_from_garrow K C (garrow_from_reification K C reification).
+  Definition step1_niso
+    `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (reification : Reification K ce (enr_c_i ce))
+    : reification_rstar reification ≃ (RestrictToImage reification >>>> R' K CM reification >>>> FullImage_InclusionFunctor CM).
+    exists (fun c1 => homset_tensor_iso K CM reification c1).
+    intros.
     simpl.
-    unfold mon_f.
-    unfold garrow_functor.
-    apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))).
-       apply (@step1_niso _ K _ _ C reification).
-       apply (if_inv (roundtrip_lemma K C reification)).
+    etransitivity.
+    eapply comp_respects; [ apply reflexivity | idtac ].
+    apply associativity.
+    apply iso_comp1_right.
     Qed.
 
   Lemma roundtrip_garrow_to_garrow
-    `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (garrow : GeneralizedArrow K C)
-    : garrow ≃ garrow_from_reification K C (reification_from_garrow K C garrow).
-    apply (ffc_functor_weakly_monic _ (ffme_mf_full C) (ffme_mf_faithful C) (ffme_mf_conservative C) (ffme_mf_conservative C)).
+    `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (garrow : GeneralizedArrow K CM)
+    : garrow ≃ garrow_from_reification K C CM (reification_from_garrow K CM garrow).
+
     apply if_inv.
-    apply (if_comp(F2:=(step1_functor K C (reification_from_garrow K C garrow)
-           >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))).
-    unfold mf_f.
+    eapply if_comp.
+    eapply if_inv.
     unfold garrow_from_reification.
+    simpl.
+    unfold mf_F.
     unfold garrow_functor.
-    unfold step2_functor.
-    set (@roundtrip_lemma _ K _ _ C) as q.
-    apply (q (reification_from_garrow K C garrow)).
+    apply (if_associativity
+      (RestrictToImage (reification_from_garrow K CM garrow))
+      (R' K CM (reification_from_garrow K CM garrow))
+      (step2_functor C)).
+
+    apply (ffc_functor_weakly_monic _ me_full me_faithful me_conservative me_conservative).
+    eapply if_comp.
+    apply (if_associativity
+      (RestrictToImage (reification_from_garrow K CM garrow) >>>> R' K CM (reification_from_garrow K CM garrow))
+      (step2_functor C)
+      me_homfunctor).
+
+    set ((R' K CM (reification_from_garrow K CM garrow))) as f.
+    unfold HomFunctor_fullimage in f.
+    set (roundtrip_lemma (me_full(MonicEnrichment:=C))) as q.
+    set (q (me_faithful(MonicEnrichment:=C)) _ _ _ _ f) as q'.
+
+    eapply if_comp.
+      apply (if_associativity (RestrictToImage (reification_from_garrow K CM garrow)) f (step2_functor C >>>> me_homfunctor)).
+      unfold step2_functor.
+      eapply if_comp.
+      apply (if_respects
+        (RestrictToImage (reification_from_garrow K CM garrow))
+        (RestrictToImage (reification_from_garrow K CM garrow))
+        _ _ (if_id _) q').
+
+    eapply if_comp.
+      eapply if_inv.
+      apply (if_associativity (RestrictToImage (reification_from_garrow K CM garrow)) f (FullImage_InclusionFunctor me_homfunctor)).
+
     apply if_inv.
-    apply (step1_niso K C (reification_from_garrow K C garrow)).
-    Qed.
+      apply (step1_niso K C CM (reification_from_garrow K CM garrow)).
+      Qed.
+
+  Lemma roundtrip_reification_to_reification
+    `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (reification : Reification K ce (enr_c_i ce))
+    : reification ≃ reification_from_garrow K CM (garrow_from_reification K C CM reification).
+
+    simpl.
+      unfold garrow_functor.
+
+    eapply if_comp.
+      apply (step1_niso K C CM reification).
+
+    unfold garrow_monoidal.
+      unfold mf_F.
+      apply if_inv.
+      eapply if_comp.
+      apply (if_associativity (RestrictToImage reification) (R' K CM reification >>>> step2_functor C)
+        (HomFunctor ce (pmon_I (enr_c_pm ce)))).
+      apply if_inv.
+      eapply if_comp.
+      apply (if_associativity (RestrictToImage reification) (R' K CM reification)
+        (FullImage_InclusionFunctor (HomFunctor ce (pmon_I (enr_c_pm ce))))).
+
+    apply (if_respects (RestrictToImage reification) (RestrictToImage reification) _ _ (if_id _)).
+      apply if_inv.
+      eapply if_comp.
+      apply (if_associativity  (R' K CM reification) (step2_functor C) (HomFunctor ce _)).
+
+    set ((R' K CM reification)) as f.
+      unfold HomFunctor_fullimage in f.
+      set (roundtrip_lemma (me_full(MonicEnrichment:=C))) as q.
+      set (q (me_faithful(MonicEnrichment:=C)) _ _ _ _ f) as q'.
+      apply q'.
+      Qed.
 
 End ReificationsEquivalentToGeneralizedArrows.