almost finished with main theorem

diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v
index a9bedbb..3ec6660 100644 (file)
--- a/src/GeneralizedArrowCategory.v
+++ b/src/GeneralizedArrowCategory.v
@@ -26,19 +26,36 @@ Require Import GeneralizedArrow.
 Require Import WeakFunctorCategory.
 Require Import SmallSMMEs.
 
 Require Import WeakFunctorCategory.
 Require Import SmallSMMEs.
 

+(*
+ * Technically reifications form merely a *semicategory* (no identity
+ * maps), but one can always freely adjoin identity maps (and nothing
+ * else) to a semicategory to get a category whose non-identity-map
+ * portion is identical to the original semicategory
+ *
+ * Also, technically this category has ALL enrichments (not just the
+ * surjective monic monoidal ones), though there maps OUT OF only the
+ * surjective enrichments and INTO only the monic monoidal
+ * enrichments.  It's a big pain to do this in Coq, but sort of might
+ * matter in real life: a language with really severe substructural
+ * restrictions might fail to be monoidally enriched, meaning we can't
+ * use it as a host language.  But that's for the next paper...
+ *)

 Inductive GeneralizedArrowOrIdentity : SMMEs -> SMMEs -> Type :=
   | gaoi_id   : forall smme:SMMEs,                             GeneralizedArrowOrIdentity smme smme
   | gaoi_ga : forall s1 s2:SMMEs, GeneralizedArrow s1 s2  -> GeneralizedArrowOrIdentity s1   s2.
 
 Inductive GeneralizedArrowOrIdentity : SMMEs -> SMMEs -> Type :=
   | gaoi_id   : forall smme:SMMEs,                             GeneralizedArrowOrIdentity smme smme
   | gaoi_ga : forall s1 s2:SMMEs, GeneralizedArrow s1 s2  -> GeneralizedArrowOrIdentity s1   s2.
 

-Definition generalizedArrowOrIdentityFunc
-  : forall s1 s2, GeneralizedArrowOrIdentity s1 s2 -> { fobj : _ & Functor s1 s2 fobj }.
-  intros.
-  destruct X.
-  exists (fun x => x).
-  apply functor_id.
-  eapply existT.
-  apply (g >>>> RepresentableFunctor s2 (mon_i s2)).
-  Defined.
+Definition generalizedArrowOrIdentityFobj (s1 s2:SMMEs) (f:GeneralizedArrowOrIdentity s1 s2) : s1 -> s2 :=
+  match f in GeneralizedArrowOrIdentity S1 S2 return S1 -> S2 with
+  | gaoi_id  s       => fun x => x
+  | gaoi_ga s1 s2 f  => fun a => ehom(ECategory:=s2) (mon_i (smme_mon s2)) (ga_functor_obj f a)
+  end.
+
+Definition generalizedArrowOrIdentityFunc s1 s2 (f:GeneralizedArrowOrIdentity s1 s2)
+  : Functor s1 s2 (generalizedArrowOrIdentityFobj _ _ f) :=
+  match f with
+  | gaoi_id  s       => functor_id _
+  | gaoi_ga s1 s2 f  => ga_functor f >>>> RepresentableFunctor s2 (mon_i s2)
+  end.

 
 Definition compose_generalizedArrows (s0 s1 s2:SMMEs) :
   GeneralizedArrow s0 s1 -> GeneralizedArrow s1 s2 -> GeneralizedArrow s0 s2.
 
 Definition compose_generalizedArrows (s0 s1 s2:SMMEs) :
   GeneralizedArrow s0 s1 -> GeneralizedArrow s1 s2 -> GeneralizedArrow s0 s2.

@@ -66,7 +83,7 @@ Definition generalizedArrowOrIdentityComp
 Definition MorphismsOfCategoryOfGeneralizedArrows : @SmallFunctors SMMEs.
   refine {| small_func      := GeneralizedArrowOrIdentity
           ; small_func_id   := fun s => gaoi_id s
 Definition MorphismsOfCategoryOfGeneralizedArrows : @SmallFunctors SMMEs.
   refine {| small_func      := GeneralizedArrowOrIdentity
           ; small_func_id   := fun s => gaoi_id s

-          ; small_func_func := fun smme1 smme2 f => projT2 (generalizedArrowOrIdentityFunc _ _ f)
+          ; small_func_func := fun smme1 smme2 f => generalizedArrowOrIdentityFunc _ _ f

           ; small_func_comp := generalizedArrowOrIdentityComp
          |}; intros; simpl.
   apply if_id.
           ; small_func_comp := generalizedArrowOrIdentityComp
          |}; intros; simpl.
   apply if_id.

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index f17caa5..627aa22 100644 (file)
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -107,14 +107,6 @@ Section GArrowFromReification.
       apply (fmor_preserves_comp reification)).
       Defined.
 
       apply (fmor_preserves_comp reification)).
       Defined.
 

-(*
-  Definition FullImage_Monoidal 
-    `(F:@Functor Cobj CHom C1 Dobj DHom D1 Fobj) `(mc:MonoidalCat D1 Mobj MF) : MonoidalCat (FullImage F) Mobj.
-
-  Definition step1_functor_monoidal : MonoidalFunctor (enr_v_mon K) step1_functor.
-    admit.
-    Defined.
-*)

   Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C))).
     exists (fun c1 => homset_tensor_iso c1).
     abstract (intros;
   Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C))).
     exists (fun c1 => homset_tensor_iso c1).
     abstract (intros;

@@ -130,15 +122,30 @@ Section GArrowFromReification.
 
   Definition garrow_functor := step1_functor >>>> step2_functor.
 
 
   Definition garrow_functor := step1_functor >>>> step2_functor.
 

-  Definition garrow_from_reification : GeneralizedArrow K C.
-    refine {| ga_functor := garrow_functor |}.
-    (*
-    unfold garrow_functor.
-    apply MonoidalFunctorsCompose.
-    apply MonoidalFunctorsCompose.
-    *)
+  Lemma garrow_functor_monoidal_niso
+    : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor.
+    admit.
+    Defined.
+  Lemma garrow_functor_monoidal_iso
+    : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)).
+    admit.
+    Defined.
+
+  Instance garrow_functor_monoidal : MonoidalFunctor (enr_v_mon K) C garrow_functor :=
+    { mf_coherence := garrow_functor_monoidal_niso
+    ; mf_id        := garrow_functor_monoidal_iso
+    }.
+    admit.
+    admit.

     admit.
     Defined.
 
     admit.
     Defined.
 

+  Definition garrow_from_reification : GeneralizedArrow K C.
+    refine
+      {| ga_functor          := garrow_functor
+       ; ga_functor_monoidal := garrow_functor_monoidal
+      |}.
+    Defined.
+

 End GArrowFromReification.
 Opaque homset_tensor_iso.
 End GArrowFromReification.
 Opaque homset_tensor_iso.

diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
index f735679..0227f60 100644 (file)
--- a/src/ReificationCategory.v
+++ b/src/ReificationCategory.v
@@ -26,6 +26,19 @@ Require Import Reification.
 Require Import WeakFunctorCategory.
 Require Import SmallSMMEs.
 
 Require Import WeakFunctorCategory.
 Require Import SmallSMMEs.
 

+(* Technically reifications form merely a *semicategory* (no identity
+ * maps), but one can always freely adjoin identity maps (and nothing
+ * else) to a semicategory to get a category whose non-identity-map
+ * portion is identical to the original semicategory
+ *
+ * Also, technically this category has ALL enrichments (not just the
+ * surjective monic monoidal ones), though there maps OUT OF only the
+ * surjective enrichments and INTO only the monic monoidal
+ * enrichments.  It's a big pain to do this in Coq, but sort of might
+ * matter in real life: a language with really severe substructural
+ * restrictions might fail to be monoidally enriched, meaning we can't
+ * use it as a host language.  But that's for the next paper...
+ *)

 Inductive ReificationOrIdentity : SMMEs -> SMMEs -> Type :=
   | roi_id   : forall smme:SMMEs,                                  ReificationOrIdentity smme smme
   | roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (mon_i s2) -> ReificationOrIdentity s1   s2.
 Inductive ReificationOrIdentity : SMMEs -> SMMEs -> Type :=
   | roi_id   : forall smme:SMMEs,                                  ReificationOrIdentity smme smme
   | roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (mon_i s2) -> ReificationOrIdentity s1   s2.

@@ -49,7 +62,8 @@ Definition compose_reifications (s0 s1 s2:SMMEs) :
   Reification s0 s1 (mon_i s1) -> Reification s1 s2 (mon_i s2) -> Reification s0 s2 (mon_i s2).
   intros.
   refine
   Reification s0 s1 (mon_i s1) -> Reification s1 s2 (mon_i s2) -> Reification s0 s2 (mon_i s2).
   intros.
   refine

-    {| reification_rstar   := MonoidalFunctorsCompose _ _ _ _ _ (reification_rstar X) (reification_rstar X0)
+    {| reification_rstar_f := reification_rstar_f X >>>> reification_rstar_f X0
+     ; reification_rstar   := MonoidalFunctorsCompose _ _ _ _ _ (reification_rstar X) (reification_rstar X0)

      ; reification_r       := fun K => (reification_r X K) >>>> (reification_r X0 (mon_i s1))
     |}.
   intro K.
      ; reification_r       := fun K => (reification_r X K) >>>> (reification_r X0 (mon_i s1))
     |}.
   intro K.

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.
 
 Require Import ReificationsEquivalentToGeneralizedArrows.
 Require Import WeakFunctorCategory.
 

-

 Section ReificationsIsomorphicToGeneralizedArrows.
 
 Section ReificationsIsomorphicToGeneralizedArrows.
 

-    Definition M1 (c1 c2 : SmallSMMEs.SMMEs) :
+    Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :

       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
       intro GA.
       (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
       (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
       intro GA.

@@ -43,6 +42,48 @@ Section ReificationsIsomorphicToGeneralizedArrows.
       apply g.
       Defined.
 
       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).
     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.
 
       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.
 
     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.
 
 End ReificationsIsomorphicToGeneralizedArrows.