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

diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v
index dc2f6b0..8edd1e0 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.                              *)
 (*                                                                                                                               *)
 (*********************************************************************************************************************************)
 
@@ -27,13 +27,14 @@ 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.
 
 Section ReificationsIsomorphicToGeneralizedArrows.
 
-    Definition M1 (c1 c2 : SmallSMMEs.SMMEs) :
+    Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
       intro GA.
@@ -43,6 +44,104 @@ Section ReificationsIsomorphicToGeneralizedArrows.
       apply 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').
+      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').
+      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).
+      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 >>>> HomFunctor s0 (mon_i s0))) (ga_functor g) (HomFunctor s2 (me_i s2))).
+        Defined.
+
     Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
@@ -52,35 +151,107 @@ Section ReificationsIsomorphicToGeneralizedArrows.
       apply (garrow_from_reification s1 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) 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 q.
+        apply if_id.
+      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
 
-    Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
-      apply WeakFunctorCategoriesIsomorphic with (M1:=M1) (M2:=M2).
-      destruct g.
+    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.
+        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.
+
+    Lemma M2_respects :
+      forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
+         f ~~ f' ->
+         M2 a b f ~~ M2 a b f'.
       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.
+        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.
+        apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
+        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))).
+        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; 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 *.
+      apply (eqv1 _ _ f f'); auto.
+      unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
+      apply (eqv2 _ _ f f'); auto.
       Qed.
 
 End ReificationsIsomorphicToGeneralizedArrows.