X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FReificationsIsomorphicToGeneralizedArrows.v;h=54d911a8ea76a7d37567c1cc2ee736bb7b0485f6;hb=916f33924e493c9be8290d0aadc35cf85d6899af;hp=12304542a1f610d3d87be536d195ff27c9139add;hpb=64d416692bda1d36c33b5efa245d46dcf546ad4a;p=coq-hetmet.git

diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v
index 1230454..54d911a 100644
--- a/src/ReificationsIsomorphicToGeneralizedArrows.v
+++ b/src/ReificationsIsomorphicToGeneralizedArrows.v
@@ -212,7 +212,6 @@ Section ReificationsIsomorphicToGeneralizedArrows.
           eapply if_comp.
           apply (step1_niso smme (smme_mee smme) (smme_mon smme) x).
           apply if_inv.
-          set (roundtrip_lemma smme (smme_mee smme) (smme_mon smme) x) as q.
           apply if_inv.
           eapply if_comp.
           apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
@@ -224,9 +223,17 @@ Section ReificationsIsomorphicToGeneralizedArrows.
           apply (if_respects (RestrictToImage x) (RestrictToImage x)).
           apply (if_id (RestrictToImage x)).
           unfold mf_F.
-          unfold me_homfunctor in q.
-          unfold pmon_I.
-          apply q.
+          eapply if_comp.
+            apply (if_associativity (R' smme smme x) (ff_functor_section_functor me_homfunctor me_full me_faithful)
+              (HomFunctor (senr_c smme) (senr_c_i smme))).
+          set (roundtrip_lemma (me_full(MonicEnrichment:=smme_mee smme))) as q.
+          set (R' smme smme x) as f.
+          set (me_faithful(MonicEnrichment:=smme_mee smme)) as ff.
+          unfold HomFunctor_fullimage in f.
+          unfold mf_F in f.
+          set (q ff _ _ (FullImage x) _ f) as q'.
+          unfold me_homfunctor in q'.
+          exact q'.
 
       simpl in *.
         destruct f'; simpl in *.
@@ -253,11 +260,19 @@ Section ReificationsIsomorphicToGeneralizedArrows.
         apply (if_id (RestrictToImage x)).
 
         unfold mf_F.
-        set (roundtrip_lemma smme (smme_mee smme) (smme_mon smme) x) as q.
         apply if_inv.
-        unfold me_homfunctor in q.
-        unfold pmon_I.
-        apply q.
+
+        eapply if_comp.
+          apply (if_associativity (R' smme smme x) (ff_functor_section_functor me_homfunctor me_full me_faithful)
+            (HomFunctor (senr_c smme) (senr_c_i smme))).
+        set (roundtrip_lemma (me_full(MonicEnrichment:=smme_mee smme))) as q.
+          set (R' smme smme x) as f.
+          set (me_faithful(MonicEnrichment:=smme_mee smme)) as ff.
+          unfold HomFunctor_fullimage in f.
+          unfold mf_F in f.
+          set (q ff _ _ (FullImage x) _ f) as q'.
+          unfold me_homfunctor in q'.
+          exact q'.
 
       simpl in *.
         unfold garrow_functor.