almost finished with main theorem

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

diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v
index dc2f6b0..5163c26 100644 (file)
--- a/src/ReificationsIsomorphicToGeneralizedArrows.v
+++ b/src/ReificationsIsomorphicToGeneralizedArrows.v
@@ -30,10 +30,9 @@ Require Import GeneralizedArrowCategory.
 Require Import ReificationsEquivalentToGeneralizedArrows.
 Require Import WeakFunctorCategory.
 
-
 Section ReificationsIsomorphicToGeneralizedArrows.
 
-    Definition M1 (c1 c2 : SmallSMMEs.SMMEs) :
+    Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
       intro GA.
@@ -43,6 +42,48 @@ Section ReificationsIsomorphicToGeneralizedArrows.
       apply g.
       Defined.
 
+    Lemma invert_ga : forall (a: SMME)
+      (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
+      (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
+      admit.
+      Qed.
+
+    Lemma invert_reif : forall (a: SMME)
+      (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
+      (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
+      admit.
+      Qed.
+
+    Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
+      refine {| fmor := fun a b f => M1 f |}.
+      intros.
+        unfold hom in *.
+        unfold eqv in *.
+        simpl in *.
+        destruct f.
+        set (invert_ga _ f') as q.
+        destruct q; subst.
+        apply if_id.
+        simpl in *.
+        destruct H0; subst.
+        apply H.
+        simpl in *.
+        destruct f'; simpl in *.
+        apply H.
+        apply H.
+      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_associativity 
+          ((ga_functor g0 >>>> RepresentableFunctor s0 (mon_i s0))) (ga_functor g) (RepresentableFunctor s2 (me_i s2))).
+        Defined.
+
     Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
@@ -52,35 +93,101 @@ Section ReificationsIsomorphicToGeneralizedArrows.
       apply (garrow_from_reification s1 s2 r).
       Defined.
 
-    (*
+    Lemma M2_respects :
+      forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
+         f ~~ f' ->
+         M2 a b f ~~ M2 a b f'.
+      intros.
+        unfold hom in *.
+        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).
+      simpl in *.
+        destruct f'; simpl in *.
+        apply if_inv.
+        apply if_inv in H.
+        apply (if_comp 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).
+      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)).
+        apply if_inv.
+        apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
+        apply yy'.
+        Qed.
 
-     * Oh my, this is massively embarrassing.  In the paper I claim
-     * that Generalized Arrows form a category and Reifications form a
-     * category, when in fact they form merely a SEMIcategory (see
-     * http://ncatlab.org/nlab/show/semicategory) since we cannot be sure that the identity functor on the
+    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.
 
     Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
-      apply WeakFunctorCategoriesIsomorphic with (M1:=M1) (M2:=M2).
-      destruct g.
-      intros.
-      simpl.
-      simpl in H.
-      split f.
-      destruct f.
-      dependent destruction f.
-      intros until g.
-      destruct f.
-      simpl.
-      inversion g.
-      destruct f as [ ] _eqn.
-      destruct g as [ ] _eqn.
-      destruct g.
-      subst.
-      simpl.
-      case g.
-      simpl.
-      inversion g; subst; intros.
-      destruct g.
-      Qed.
+      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.
+        
+      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.
 
 End ReificationsIsomorphicToGeneralizedArrows.