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

diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v
index 5163c26..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,8 +27,10 @@ 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.
 
@@ -42,16 +44,72 @@ 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').
-      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).
@@ -81,7 +139,7 @@ Section ReificationsIsomorphicToGeneralizedArrows.
         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))).
+          ((ga_functor g0 >>>> HomFunctor s0 (mon_i s0))) (ga_functor g) (HomFunctor s2 (me_i s2))).
         Defined.
 
     Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
@@ -93,6 +151,44 @@ 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.
+
+
+    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' ->
@@ -130,64 +226,32 @@ Section ReificationsIsomorphicToGeneralizedArrows.
         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'.
+        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.
-        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.