X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsAndGeneralizedArrows.v;h=6a615aca9effe6da6c4ede86ebd3c3fbddb0386b;hp=d59b030545f4f767cf2fc097970fbbe624516840;hb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f;hpb=b096aab78240e38ff69c120367e65be60cbc54f5

diff --git a/src/ReificationsAndGeneralizedArrows.v b/src/ReificationsAndGeneralizedArrows.v
index d59b030..6a615ac 100644
--- a/src/ReificationsAndGeneralizedArrows.v
+++ b/src/ReificationsAndGeneralizedArrows.v
@@ -1,7 +1,8 @@
 (*********************************************************************************************************************************)
 (* ReificationsAndGeneralizedArrows:                                                                                             *)
 (*                                                                                                                               *)
-(*   The category of generalized arrows and the category of reifications are equivalent categories.                              *)
+(*   For each pair of enrichments E1 and E2, there is a bijection between the generalized arrows E1->E2 and the reifications     *)
+(*   E1->E2                                                                                                                      *)
 (*                                                                                                                               *)
 (*********************************************************************************************************************************)
 
@@ -53,7 +54,7 @@ Section ReificationsEquivalentToGeneralizedArrows.
 
   Definition roundtrip_lemma
     `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
-    := roundtrip_lemma' (RepresentableFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification).
+    := 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))
@@ -61,7 +62,7 @@ Section ReificationsEquivalentToGeneralizedArrows.
     simpl.
     unfold mon_f.
     unfold garrow_functor.
-    apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).
+    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)).
     Qed.
@@ -69,10 +70,10 @@ Section ReificationsEquivalentToGeneralizedArrows.
   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_conservative C)).
+    apply (ffc_functor_weakly_monic _ (ffme_mf_full C) (ffme_mf_faithful C) (ffme_mf_conservative C) (ffme_mf_conservative C)).
     apply if_inv.
     apply (if_comp(F2:=(step1_functor K C (reification_from_garrow K C garrow)
-           >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).
+           >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))).
     unfold mf_f.
     unfold garrow_from_reification.
     unfold garrow_functor.