X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsIsomorphicToGeneralizedArrows.v;h=b95f30f8078fbdadd9c5b0d567fb0248ba6543f0;hp=5163c2680917a385dd58789c3ac01b8adbb603f7;hb=423b0bd3972c5bcbbd757cb715e13b5b9104a9a6;hpb=d2526b193694dd7a5c7ab9d80d6b6656a7459bb9

diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v
index 5163c26..b95f30f 100644
--- a/src/ReificationsIsomorphicToGeneralizedArrows.v
+++ b/src/ReificationsIsomorphicToGeneralizedArrows.v
@@ -1,7 +1,7 @@
 (*********************************************************************************************************************************)
-(* ReificationsEquivalentToGeneralizedArrows:                                                                                    *)
+(* ReificationsIsomorphicToGeneralizedArrows:                                                                                    *)
 (*                                                                                                                               *)
-(*   The category of generalized arrows and the category of reifications are equivalent categories.                              *)
+(*   The category of generalized arrows and the category of reifications are isomorphic categories.                              *)
 (*                                                                                                                               *)
 (*********************************************************************************************************************************)
 
@@ -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.
@@ -27,31 +27,89 @@ Require Import GeneralizedArrowFromReification.
 Require Import ReificationFromGeneralizedArrow.
 Require Import ReificationCategory.
 Require Import GeneralizedArrowCategory.
-Require Import ReificationsEquivalentToGeneralizedArrows.
+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 *)
+    Require Import Coq.Logic.Eqdep.
+
+    Inductive Heq : forall {A}{B}, A -> B -> Prop :=
+      heq : forall {A} (a:A), Heq a a.
+
+    Lemma invert_ga' : forall (a b: SMME)
+      (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>b), a=b ->
+      (Heq f (gaoi_id a)) \/ (exists f', Heq f (gaoi_ga a b f')).
+      intros.
+      destruct f.
+      left; apply heq.
+      subst; right.
+      exists g.
+      apply heq.
       Defined.
 
     Lemma invert_ga : forall (a: SMME)
       (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
       (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
-      admit.
+      intros.
+      set (invert_ga' a a f (refl_equal a)) as q.
+      destruct q.
+      left.
+      inversion H.
+      apply inj_pairT2 in H2.
+      apply inj_pairT2 in H1.
+      subst; auto.
+      right.
+      destruct H.
+      exists x.
+      inversion H.
+      apply inj_pairT2 in H2.
+      apply inj_pairT2 in H1.
+      subst; auto.
       Qed.
 
+    Lemma invert_reif' : forall (a b: SMME)
+      (f:a~~{MorphismsOfCategoryOfReifications}~~>b), a=b ->
+      (Heq f (roi_id a)) \/ (exists f', Heq f (roi_reif a b f')).
+      intros.
+      destruct f.
+      left; apply heq.
+      subst; right.
+      exists r.
+      apply heq.
+      Defined.
+
     Lemma invert_reif : forall (a: SMME)
       (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
       (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
-      admit.
+      intros.
+      set (invert_reif' a a f (refl_equal a)) as q.
+      destruct q.
+      left.
+      inversion H.
+      apply inj_pairT2 in H2.
+      apply inj_pairT2 in H1.
+      subst; auto.
+      right.
+      destruct H.
+      exists x.
+      inversion H.
+      apply inj_pairT2 in H2.
+      apply inj_pairT2 in H1.
+      subst; auto.
       Qed.
 
     Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
@@ -79,20 +137,58 @@ Section ReificationsIsomorphicToGeneralizedArrows.
         apply if_id.
         destruct g; simpl.
         apply if_id.
-        unfold mf_f; simpl.
+        simpl.
         apply (if_associativity 
-          ((ga_functor g0 >>>> RepresentableFunctor s0 (mon_i s0))) (ga_functor g) (RepresentableFunctor 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)
+      (f' : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)
+      (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 (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.
+        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.
+
+    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 (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.
+        simpl in q.
+        simpl in q.
+        apply q.
+        Qed.
+
     Lemma M2_respects :
       forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
          f ~~ f' ->
@@ -102,92 +198,170 @@ 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.
+          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.
+          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 *.
-        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.
+        apply if_inv.
+
+        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.
         unfold step2_functor.
-        apply if_inv in H.
-        set (if_comp H (@step1_niso _ s1 _ _ s2 r)) as yy.
-        set (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) yy) as yy'.
-        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.
-        apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
-        apply yy'.
+        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 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
+          (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.
+        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).
       refine {| fmor := fun a b f => M2 _ _ f |}.
       apply M2_respects.
       intros; simpl; apply if_id.
-      intros.
-        simpl.
-        destruct f; simpl.
-        apply if_id.
-        destruct g; simpl.
-        apply if_id.
-        unfold mf_f; simpl.
-        apply (if_respects
-          (F0:=((garrow_functor s1 s0 r >>>> RepresentableFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0))
-          (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0)))
-          (G0:=(RepresentableFunctor s2 (mon_i s2)))
-          (G1:=(RepresentableFunctor s2 (mon_i s2))));
-        [ idtac | apply if_id ].
-        admit.
-        Defined.
+      intros; apply (@bijection_lemma _ _ _ _ _ M1_Functor M2); intros.
+      apply M2_respects; auto.
+      unfold fmor; simpl.
+      apply (@eqv1 _ _ f0 f0).
+      apply if_id.
+      unfold fmor; simpl.
+      apply (@eqv2 _ _ f0 f0).
+      apply if_id.
+      Defined.
 
     Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
       refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
-        unfold hom in *.
-        set (@roundtrip_garrow_to_garrow _ a _ _ 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:=RepresentableFunctor s2 (mon_i s2))(G1:=RepresentableFunctor s2 (mon_i s2))).
-        apply q.
-        apply if_id.
-        
+      apply (eqv1 _ _ f f'); auto.
       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
-        unfold hom in *.
-        set (@roundtrip_reification_to_reification _ a _ _ 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.
+      apply (eqv2 _ _ f f'); auto.
+      Qed.
 
 End ReificationsIsomorphicToGeneralizedArrows.