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

diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v
index 8edd1e0..1230454 100644
--- a/src/ReificationsIsomorphicToGeneralizedArrows.v
+++ b/src/ReificationsIsomorphicToGeneralizedArrows.v
@@ -17,9 +17,9 @@ Require Import Enrichment_ch2_8.
 Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
+Require Import PreMonoidalCategories.
 Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
-Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 Require Import Reification.
 Require Import GeneralizedArrow.
@@ -31,17 +31,17 @@ Require Import ReificationCategory.
 Require Import ReificationsAndGeneralizedArrows.
 Require Import WeakFunctorCategory.
 Require Import BijectionLemma.
+Require Import Enrichments.
 
 Section ReificationsIsomorphicToGeneralizedArrows.
 
-    Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
+    Definition M1 {c1 c2 : SMMEs} :
       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
       intro GA.
       destruct GA; [ apply roi_id | idtac ].
       apply roi_reif.
-      apply reification_from_garrow.
-      apply g.
+      apply (reification_from_garrow s1 s2 g).
       Defined.
 
     (* I tried really hard to avoid this *)
@@ -137,18 +137,18 @@ Section ReificationsIsomorphicToGeneralizedArrows.
         apply if_id.
         destruct g; simpl.
         apply if_id.
-        unfold mf_f; simpl.
+        simpl.
         apply (if_associativity 
-          ((ga_functor g0 >>>> HomFunctor s0 (mon_i s0))) (ga_functor g) (HomFunctor s2 (me_i s2))).
+          ((ga_functor g0 >>>> HomFunctor s0 (enr_c_i s0))) (ga_functor g) (HomFunctor s2 (enr_c_i s2))).
         Defined.
 
-    Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
+    Definition M2 (c1 c2 : SMMEs) :
       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
       intro RE.
       destruct RE; [ apply gaoi_id | idtac ].
       apply gaoi_ga.
-      apply (garrow_from_reification s1 s2 r).
+      apply (garrow_from_reification s1 (smme_mee s2) s2 r).
       Defined.
 
     Lemma eqv1 a b (f : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)
@@ -156,38 +156,38 @@ Section ReificationsIsomorphicToGeneralizedArrows.
       (H : generalizedArrowOrIdentityFunc a b f ≃ generalizedArrowOrIdentityFunc a b f') :
       generalizedArrowOrIdentityFunc a b (M2 a b (M1 f)) ≃ generalizedArrowOrIdentityFunc a b f'.
         unfold hom in *.
-        set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
+        set (@roundtrip_garrow_to_garrow a b (smme_mee b) (smme_mon b)) as q.
         destruct f; simpl in *.
         apply H.
         apply if_inv.
         apply (if_comp (if_inv H)).
         clear H.
-        unfold mf_f in q.
-        apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
-          (G0:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor s2 (mon_i s2))).
+        apply (if_respects
+          (ga_functor g)
+          (garrow_functor s1 (smme_mee s2) s2 (reification_from_garrow s1 s2 g))
+          (HomFunctor (senr_c s2) (senr_c_i s2))
+          (HomFunctor (senr_c s2) (senr_c_i s2))
+        ).
         apply q.
         apply if_id.
-      Qed.
-
+        Qed.
 
     Lemma eqv2 a b (f : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
       (f' : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
       (H : reificationOrIdentityFunc a b f ≃ reificationOrIdentityFunc a b f') :
       reificationOrIdentityFunc _ _ (M1 (M2 _ _ f)) ≃ reificationOrIdentityFunc _ _ f'.
         unfold hom in *.
-        set (@roundtrip_reification_to_reification _ a _ _ b) as q.
+        set (@roundtrip_reification_to_reification a b (smme_mee b) (smme_mon b)) as q.
         destruct f; simpl.
         apply H.
         apply if_inv.
         apply (if_comp (if_inv H)).
         clear H.
         simpl.
-        unfold mf_f; simpl.
         simpl in q.
-        unfold mf_f in q.
         simpl in q.
         apply q.
-      Qed.
+        Qed.
 
     Lemma M2_respects :
       forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
@@ -198,38 +198,109 @@ Section ReificationsIsomorphicToGeneralizedArrows.
         unfold eqv in *.
         simpl in *.
         destruct f.
-        set (invert_reif _ f') as q.
-        destruct q; subst.
-        apply if_id.
-        simpl in *.
-        destruct H0; subst.
-        simpl in *.
-        unfold garrow_functor.
-        unfold step2_functor.
-        apply (if_comp H).
-        clear H.
-        apply (if_comp (@step1_niso _ smme _ _ smme x)).
-        apply if_inv.
-        apply (@roundtrip_lemma _ smme _ _ smme x).
+          set (invert_reif _ f') as q.
+          destruct q; subst.
+          apply if_id.
+
+          simpl in *.
+          destruct H0; subst.
+          simpl in *.
+          unfold garrow_functor.
+          unfold step2_functor.
+          apply (if_comp H).
+          clear H.
+          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 _)).
+          apply if_inv.
+          eapply if_comp.
+          apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
+                   ff_functor_section_functor me_homfunctor me_full me_faithful))
+          (HomFunctor (senr_c smme) (senr_c_i smme))).
+          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.
+
       simpl in *.
         destruct f'; simpl in *.
-        apply if_inv.
+        simpl in *.
         apply if_inv in H.
-        apply (if_comp H).
+        eapply if_comp; [ idtac | eapply if_inv; apply H ].
         clear H.
         unfold garrow_functor.
         unfold step2_functor.
-        apply (if_comp (@step1_niso _ smme _ _ smme r)).
         apply if_inv.
-        apply (@roundtrip_lemma _ smme _ _ smme r).
+        eapply if_comp.
+        apply (step1_niso smme (smme_mee smme) (smme_mon smme) r).
+
+        rename r into x.
+        apply if_inv.
+        eapply if_comp.
+        apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
+                 ff_functor_section_functor me_homfunctor me_full me_faithful))
+        (HomFunctor (senr_c smme) (senr_c_i smme))).
+        apply if_inv.
+        eapply if_comp.
+        apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
+        apply (if_respects (RestrictToImage x) (RestrictToImage x)).
+        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.
+
       simpl in *.
         unfold garrow_functor.
         unfold step2_functor.
-        apply if_inv in H.
-        apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
+        set (step1_niso s1 (smme_mee s2) s2 r) as q.
+        apply if_inv in q.
+        eapply if_comp.
+        eapply if_comp; [ idtac | apply q ].
+
+        eapply if_comp.
+        apply (if_associativity
+          (RestrictToImage r)
+          (R' s1 s2 r >>>> 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 r)
+          (R' s1 s2 r)
+          (FullImage_InclusionFunctor _)).
+        apply (if_respects
+          (RestrictToImage r)
+          (RestrictToImage r)
+          (R' s1 s2 r >>>> FullImage_InclusionFunctor _)
+          (((R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful) >>>>
+             HomFunctor (senr_c s2) (senr_c_i s2)))).
+        apply (if_id _).
+        apply if_inv.
+        eapply if_comp.
+        apply (if_associativity
+          (R' s1 s2 r)
+          (ff_functor_section_functor me_homfunctor me_full me_faithful)
+          (HomFunctor (senr_c s2) (senr_c_i s2))).
+        apply if_inv.
+        apply (if_respects
+          (R' s1 s2 r)
+          (R' s1 s2 r)
+          (FullImage_InclusionFunctor _)
+          ((ff_functor_section_functor me_homfunctor me_full me_faithful >>>> HomFunctor _ _))
+        ).
+        apply (if_id _).
         apply if_inv.
-        apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
-        apply (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) (if_comp H (@step1_niso _ s1 _ _ s2 r))).
+        apply (RestrictToImage_splits_niso (HomFunctor s2 (senr_c_i s2))).
         Qed.
 
     Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).