fix erroneous conclusion to penultimate lemma

[coq-hetmet.git] / src / ReificationsIsomorphicToGeneralizedArrows.v

diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v
index 1230454..b95f30f 100644 (file)
--- 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.
@@ -291,16 +306,40 @@ Section ReificationsIsomorphicToGeneralizedArrows.
           (R' s1 s2 r)
           (ff_functor_section_functor me_homfunctor me_full me_faithful)
           (HomFunctor (senr_c s2) (senr_c_i s2))).
+        apply roundtrip_lemma.
+
+        apply if_inv.
+        set (step1_niso s1 (smme_mee s2) s2 r0) as q'.
+        apply if_inv in q'.
+        eapply if_comp.
+        eapply if_comp; [ idtac | apply q' ].
+        eapply if_comp.
+        apply (if_associativity
+          (RestrictToImage r0)
+          (R' s1 s2 r0 >>>> ff_functor_section_functor me_homfunctor me_full me_faithful)
+          (HomFunctor (senr_c s2) (senr_c_i s2))).
         apply if_inv.
+        eapply if_comp.
+        apply (if_associativity
+          (RestrictToImage r0)
+          (R' s1 s2 r0)
+          (FullImage_InclusionFunctor _)).
         apply (if_respects
-          (R' s1 s2 r)
-          (R' s1 s2 r)
-          (FullImage_InclusionFunctor _)
-          ((ff_functor_section_functor me_homfunctor me_full me_faithful >>>> HomFunctor _ _))
-        ).
+          (RestrictToImage r0)
+          (RestrictToImage r0)
+          (R' s1 s2 r0 >>>> FullImage_InclusionFunctor _)
+          (((R' s1 s2 r0 >>>> ff_functor_section_functor me_homfunctor me_full me_faithful) >>>>
+             HomFunctor (senr_c s2) (senr_c_i s2)))).
         apply (if_id _).
         apply if_inv.
-        apply (RestrictToImage_splits_niso (HomFunctor s2 (senr_c_i s2))).
+        eapply if_comp.
+        apply (if_associativity
+          (R' s1 s2 r0)
+          (ff_functor_section_functor me_homfunctor me_full me_faithful)
+          (HomFunctor (senr_c s2) (senr_c_i s2))).
+        apply roundtrip_lemma.
+        apply if_inv.
+        apply H.
         Qed.
 
     Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).