checkpoint

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 05d059a..dbeb3cc 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -40,7 +40,7 @@ Require Import HaskProofCategory.
 (*
 Require Import HaskStrongCategory.
 *)
-Require Import ReificationsEquivalentToGeneralizedArrows.
+Require Import ReificationsIsomorphicToGeneralizedArrows.
 
 Open Scope string_scope.
 Extraction Language Haskell.

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index e6d3cbd..f17caa5 100644 (file)
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -107,6 +107,14 @@ Section GArrowFromReification.
       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;
@@ -124,6 +132,11 @@ Section GArrowFromReification.
 
   Definition garrow_from_reification : GeneralizedArrow K C.
     refine {| ga_functor := garrow_functor |}.
+    (*
+    unfold garrow_functor.
+    apply MonoidalFunctorsCompose.
+    apply MonoidalFunctorsCompose.
+    *)
     admit.
     Defined.
 

diff --git a/src/PreCategory.v b/src/PreCategory.v
new file mode 100644 (file)
index 0000000..7418261
--- /dev/null
+++ b/src/PreCategory.v
@@ -0,0 +1,93 @@
+(*********************************************************************************************************************************)
+(* SemiCategory:                                                                                                                 *)
+(*                                                                                                                               *)
+(*   Same as a category, but without identity maps.   See                                                                        *)
+(*                                                                                                                               *)
+(*       http://ncatlab.org/nlab/show/semicategory                                                                               *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+
+Class SemiCategory (Ob:Type)(Hom:Ob->Ob->Type) :=
+{ semi_hom              := Hom
+; semi_ob               := Ob
+; semi_comp             :  forall  {a}{b}{c}, Hom a b -> Hom b c -> Hom a c
+; semi_eqv              :  forall  a b,   (Hom a b) -> (Hom a b) -> Prop
+; semi_eqv_equivalence  :  forall  a b,   Equivalence (semi_eqv a b)
+; semi_comp_respects    :  forall  a b c, Proper (semi_eqv a b ==> semi_eqv b c ==> semi_eqv a c) (@semi_comp _ _ _)
+; semi_associativity    :
+       forall `(f:Hom a b)`(g:Hom b c)`(h:Hom c d), semi_eqv _ _ (semi_comp (semi_comp f g) h) (semi_comp f (semi_comp g h))
+}.
+Coercion semi_ob : SemiCategory >-> Sortclass.
+
+Notation "a ~->   b" := (@semi_hom  _ _ _       a b) (at level 70).
+Notation "f ~-~   g" := (@semi_eqv  _ _ _ _ _   f g) (at level 54).
+Notation "f >>->> g" := (@semi_comp _ _ _ _ _ _ f g) (at level 45).
+
+Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:SemiCategory Ob Hom)(a b:Ob) : (semi_hom a b) (semi_eqv a b)
+  reflexivity proved by  (@Equivalence_Reflexive  _ _ (semi_eqv_equivalence a b))
+  symmetry proved by     (@Equivalence_Symmetric  _ _ (semi_eqv_equivalence a b))
+  transitivity proved by (@Equivalence_Transitive _ _ (semi_eqv_equivalence a b))
+  as parametric_relation_semi_eqv.
+  Add Parametric Morphism `(c:SemiCategory Ob Hom)(a b c:Ob) : (@semi_comp _ _ _ a b c)
+  with signature (semi_eqv _ _ ==> semi_eqv _ _ ==> semi_eqv _ _) as parametric_morphism_semi_comp.
+    intros.
+    apply semi_comp_respects; auto.
+  Defined.
+
+Class SemiFunctor
+`( c1                 : SemiCategory                           )
+`( c2                 : SemiCategory                           )
+( fobj                : c1 -> c2                               ) :=
+{ semifunctor_fobj         := fobj
+; semi_fmor                : forall {a b}, (a~->b) -> (fobj a)~->(fobj b)
+; semi_fmor_respects       : forall a b (f f':a~->b),   (f ~-~ f') ->        (semi_fmor f ~-~ semi_fmor f')
+; semi_fmor_preserves_comp : forall `(f:a~->b)`(g:b~->c), (semi_fmor f) >>->> (semi_fmor g) ~-~ semi_fmor (f >>->> g)
+}.
+Implicit Arguments semi_fmor [[Ob][Hom][c1][Ob0][Hom0][c2][fobj][a][b]].
+
+  (* register "fmor" so we can rewrite through it *)
+  Implicit Arguments semi_fmor                [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
+  Implicit Arguments semi_fmor_respects       [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
+  Implicit Arguments semi_fmor_preserves_comp [ Ob Hom Ob0 Hom0 c1 c2 fobj a b c ].
+  Notation "F \- f" := (semi_fmor F f) (at level 20)  : category_scope.
+  Add Parametric Morphism `(C1:SemiCategory)`(C2:SemiCategory)
+    (Fobj:C1->C2)
+    (F:SemiFunctor C1 C2 Fobj)
+    (a b:C1)
+  : (@semi_fmor _ _ C1 _ _ C2 Fobj F a b)
+  with signature ((@semi_eqv C1 _ C1 a b) ==> (@semi_eqv C2 _ C2 (Fobj a) (Fobj b))) as parametric_morphism_semi_fmor'.
+  intros; apply (@semi_fmor_respects _ _ C1 _ _ C2 Fobj F a b x y); auto.
+  Defined.
+  Coercion semifunctor_fobj : SemiFunctor >-> Funclass.
+
+Definition semifunctor_comp
+  `(C1:SemiCategory)
+  `(C2:SemiCategory)
+  `(C3:SemiCategory)
+  `(F:@SemiFunctor _ _ C1 _ _ C2 Fobj)`(G:@SemiFunctor _ _ C2 _ _ C3 Gobj) : SemiFunctor C1 C3 (Gobj ○ Fobj).
+  intros. apply (Build_SemiFunctor _ _ _ _ _ _ _ (fun a b m => semi_fmor G (semi_fmor F m))).
+  intros.
+  setoid_rewrite H.
+  reflexivity.
+  intros.
+  setoid_rewrite semi_fmor_preserves_comp; auto.
+  setoid_rewrite semi_fmor_preserves_comp; auto.
+  reflexivity.
+  Defined.
+Notation "f >>>–>>> g" := (@semifunctor_comp _ _ _ _ _ _ _ _ _ _ f _ g) (at level 20)  : category_scope.
+
+Class IsomorphicSemiCategories `(C:SemiCategory)`(D:SemiCategory) :=
+{ isc_f_obj    : C -> D
+; isc_g_obj    : D -> C
+; isc_f        : SemiFunctor C D isc_f_obj
+; isc_g        : SemiFunctor D C isc_g_obj
+; isc_forward  : forall a b (f:a~->b), semi_fmor isc_f  (semi_fmor isc_g  f) ~-~ f
+}.
+; isc_backward : isc_g >>>> isc_f ~~~~ functor_id D
+}.
+
+

diff --git a/src/Reification.v b/src/Reification.v
index a56ded8..2f2ba67 100644 (file)
--- a/src/Reification.v
+++ b/src/Reification.v
@@ -31,7 +31,7 @@ Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) :=
 ; reification_r         : forall k:K, Functor K C (reification_r_obj k)
 ; reification_rstar_f   :             Functor (enr_v K) (enr_v C) reification_rstar_obj
 ; reification_rstar     :             MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
-; reification_commutes  : forall k, reification_r k >>>> RepresentableFunctor C CI <~~~> RepresentableFunctor K k >>>> reification_rstar_f
+; reification_commutes : ∀ k, reification_r k >>>> RepresentableFunctor C CI <~~~> RepresentableFunctor K k >>>> reification_rstar_f
 }.
 Transparent RepresentableFunctor.
 Transparent functor_comp.

diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
index b4d444a..f735679 100644 (file)
--- a/src/ReificationCategory.v
+++ b/src/ReificationCategory.v
@@ -30,14 +30,19 @@ 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.
 
+Definition reificationOrIdentityFobj s1 s2 (f:ReificationOrIdentity s1 s2) : s1 -> s2 :=
+  match f with
+  | roi_id   s       => (fun x => x)
+  | roi_reif s1 s2 f => reification_rstar_obj f
+  end.
+
 Definition reificationOrIdentityFunc
-  : forall s1 s2, ReificationOrIdentity s1 s2 -> { fobj : _ & Functor s1 s2 fobj }.
+  : forall s1 s2 (f:ReificationOrIdentity s1 s2), Functor (enr_v s1) (enr_v s2) (reificationOrIdentityFobj s1 s2 f).
   intros.
-  destruct X.
-  exists (fun x => x).
+  destruct f.
   apply functor_id.
-  exists (reification_rstar_obj r).
-  apply r.
+  unfold reificationOrIdentityFobj.
+  apply (reification_rstar_f r).
   Defined.
 
 Definition compose_reifications (s0 s1 s2:SMMEs) :
@@ -54,7 +59,28 @@ Definition compose_reifications (s0 s1 s2:SMMEs) :
   clear q.
   set (reification_commutes X K) as comm1.
   set (reification_commutes X0 (mon_i s1)) as comm2.
-  admit.
+  set (RepresentableFunctor s0 K) as a in *.
+  set (reification_rstar_f X) as a' in *.
+  set (reification_rstar_f X0) as x in *.
+  set (reification_r X K) as b in *.
+  set (reification_r X0 (mon_i s1)) as c in *.
+  set (RepresentableFunctor s2 (mon_i s2)) as c' in *.
+  set (RepresentableFunctor s1 (mon_i s1)) as b' in *.
+  apply (ni_comp(F2:=b >>>> (b' >>>> x))).
+  apply (@ni_respects _ _ _ _ _ _ _ _ _ _ b _ b _ (c >>>> c') _ (b' >>>> x)).
+  apply ni_id.
+  apply comm2.
+  eapply ni_comp.
+  eapply ni_inv.
+  apply (ni_associativity b b' x).
+  eapply ni_inv.
+  eapply ni_comp.
+  eapply ni_inv.
+  apply (ni_associativity a a' x).
+  apply (@ni_respects _ _ _ _ _ _ _ _ _ _ (a >>>> a') _ (b >>>> b') _ x _ x).
+  apply ni_inv.
+  apply comm1.
+  apply ni_id.
   Defined.
 
 Definition reificationOrIdentityComp
@@ -70,7 +96,7 @@ Definition reificationOrIdentityComp
 Definition MorphismsOfCategoryOfReifications : @SmallFunctors SMMEs.
   refine {| small_func      := ReificationOrIdentity
           ; small_func_id   := fun s => roi_id s
-          ; small_func_func := fun smme1 smme2 f => projT2 (reificationOrIdentityFunc _ _ f)
+          ; small_func_func := fun smme1 smme2 f => reificationOrIdentityFunc _ _ f
           ; small_func_comp := reificationOrIdentityComp
          |}; intros; simpl.
   apply if_id.

diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v
index db11897..dc2f6b0 100644 (file)
--- a/src/ReificationsIsomorphicToGeneralizedArrows.v
+++ b/src/ReificationsIsomorphicToGeneralizedArrows.v
@@ -30,6 +30,57 @@ Require Import GeneralizedArrowCategory.
 Require Import ReificationsEquivalentToGeneralizedArrows.
 Require Import WeakFunctorCategory.
 
+
 Section ReificationsIsomorphicToGeneralizedArrows.
 
+    Definition M1 (c1 c2 : SmallSMMEs.SMMEs) :
+      (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
+      (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
+      intro GA.
+      destruct GA; [ apply roi_id | idtac ].
+      apply roi_reif.
+      apply reification_from_garrow.
+      apply g.
+      Defined.
+
+    Definition M2 (c1 c2 : SmallSMMEs.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).
+      Defined.
+
+    (*
+
+     * 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.
+      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.
+
 End ReificationsIsomorphicToGeneralizedArrows.

diff --git a/src/WeakFunctorCategory.v b/src/WeakFunctorCategory.v
index 49a5189..85ade61 100644 (file)
--- a/src/WeakFunctorCategory.v
+++ b/src/WeakFunctorCategory.v
@@ -192,8 +192,8 @@ Section WeakFunctorCategoryIsomorphism.
         apply q.
         Defined.
 
-    Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE F1 F2.
-      apply Build_IsomorphicCategories.
+    Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE.
+      refine {| ic_f := F1 ; ic_g := F2 |}.
       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
         eapply if_comp.
         apply m1_m2_id.