fill in lots of missing proofs

diff --git a/Makefile b/Makefile
index 97de58b..58f4d40 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -6,11 +6,7 @@ default: build/CoqPass.hs
 
 build/CoqPass.hs: $(allfiles)
        make build/Makefile.coq
-       cd build; make -f Makefile.coq OPT="-opt -dont-load-proofs" \
-         ExtractionMain.vo \
-         ProgrammingLanguageGeneralizedArrow.vo \
-         ProgrammingLanguageArrow.vo \
-         ProgrammingLanguageFlattening.vo
+       cd build; make -f Makefile.coq OPT="-opt -dont-load-proofs" All.vo
        cd build; make -f Makefile.coq Extraction.vo
        cat src/Extraction-prefix.hs                                     > build/CoqPass.hs
        cat build/Extraction.hs | grep -v '^module' | grep -v '^import' >> build/CoqPass.hs

diff --git a/src/All.v b/src/All.v
index b42d175..5db7ece 100644 (file)
--- a/src/All.v
+++ b/src/All.v
@@ -1,89 +1,9 @@
-Require Import Preamble.
-Require Import General.
-
-Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
-
-Require Import HaskCoreVars.
-Require Import HaskCoreTypes.
-Require Import HaskCore.
-
-Require Import HaskWeakTypes.
-Require Import HaskWeakVars.
-Require Import HaskWeak.
-
-Require Import HaskCoreToWeak.
-
-Require Import HaskStrongTypes.
-Require Import HaskStrong.
-
-Require Import NaturalDeduction.
-Require Import NaturalDeductionToLatex.
-
-Require Import HaskProof.
-
-Require Import HaskProofToStrong.
-Require Import HaskStrongToWeak.
-Require Import HaskWeakToCore.
-(*Require Import HaskWeakToStrong.*)
-Require Import HaskStrongToProof.
-(*Require Import HaskProofToLatex.*)
-
-(*Require Import HaskStrongCategory.*)
-(*Require Import Extraction.*)
-
-Require Import Categories_ch1_3.
-Require Import Functors_ch1_4.
-Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
-Require Import OppositeCategories_ch1_6_2.
-Require Import SliceCategories_ch1_6_4.
-
-Require Import EpicMonic_ch2_1.
-Require Import InitialTerminal_ch2_2.
-Require Import SectionRetract_ch2_4.
-
-Require Import Equalizers_ch3_3.
-Require Import CoEqualizers_ch3_4.
-
-Require Import Algebras_ch4.
-
-Require Import NaturalTransformations_ch7_4.
-Require Import NaturalIsomorphisms_ch7_5.
-Require Import FunctorCategories_ch7_7.
-
-Require Import Subcategories_ch7_1.
-
-Require Import Coherence_ch7_8.
-Require Import MonoidalCategories_ch7_8.
-
-Require Import Enrichment_ch2_8.
-Require Import RepresentableStructure_ch7_2.
-
-Require Import Yoneda_ch8.
-(*Require Import Exponentials_ch6.*)
-
-(*Require Import CategoryOfCategories_ch7_1.*)
-(*Require Import Adjoints_ch9.*)
-
-Require Import NaturalDeductionCategory.
-
-Require Import Reification.
-Require Import GeneralizedArrow.
-Require Import GeneralizedArrowFromReification.
-Require Import ReificationFromGeneralizedArrow.
-Require Import WeakFunctorCategory.
-Require Import SmallSMMEs.
-Require Import ReificationCategory.
-Require Import GeneralizedArrowCategory.
-Require Import ReificationsAndGeneralizedArrows.
+Require Import ExtractionMain.
+(*
+Require Import ProgrammingLanguageGeneralizedArrow.
+Require Import ProgrammingLanguageFlattening.
+Require Import ProgrammingLanguageArrow.
+Require Import ProgrammingLanguageReification.
+*)
 Require Import ReificationsIsomorphicToGeneralizedArrows.
 
-Require Import HaskProofCategory.
-Require Import ProgrammingLanguage.
-
-(* very slow! *)
-Require Import FreydCategories.
-Require Import Arrows.
-
-

diff --git a/src/Enrichments.v b/src/Enrichments.v
index a98b047..5fa684e 100644 (file)
--- a/src/Enrichments.v
+++ b/src/Enrichments.v
@@ -45,21 +45,31 @@ Structure Enrichment :=
 }.
 Coercion enr_c   : Enrichment >-> ECategory.
 
+(* Coq grinds down into a performance bog when I try to use this *)
+Definition WeaklySurjectiveEnrichment (ec:Enrichment) :=
+  @treeDecomposition (enr_v ec) (option (ec*ec))
+                  (fun t => match t with
+                            | None   => enr_v_i ec
+                            | Some x => match x with pair y z => enr_c_hom ec y z end
+                            end)
+                  (enr_v_bobj ec).
+
+(* technically this ought to be a "strictly surjective enrichment" *)
 Structure SurjectiveEnrichment :=
 { senr_c_obj      :  Type
 ; senr_v_ob       := Tree ??(senr_c_obj * senr_c_obj)
 ; senr_c_hom      := fun (c1 c2:senr_c_obj) => [(c1, c2)]
-; senr_v_hom      : senr_v_ob -> senr_v_ob -> Type
-; senr_v          : Category senr_v_ob senr_v_hom
+; senr_v_hom      :  senr_v_ob -> senr_v_ob -> Type
+; senr_v          :  Category senr_v_ob senr_v_hom
 ; senr_v_i        := []
-; senr_v_bobj     := @T_Branch (option (senr_c_obj * senr_c_obj))
-; senr_v_bin      : BinoidalCat senr_v senr_v_bobj
-; senr_v_pmon     : PreMonoidalCat senr_v_bin senr_v_i
-; senr_v_mon      : MonoidalCat senr_v_pmon
-; senr_c          : ECategory senr_v_mon senr_c_obj senr_c_hom
-; senr_c_bin      : EBinoidalCat senr_c
-; senr_c_i        : senr_c
-; senr_c_pm       : PreMonoidalCat senr_c_bin senr_c_i
+; senr_v_bobj     := @T_Branch ??(senr_c_obj * senr_c_obj)
+; senr_v_bin      :  BinoidalCat senr_v senr_v_bobj
+; senr_v_pmon     :  PreMonoidalCat senr_v_bin senr_v_i
+; senr_v_mon      :  MonoidalCat senr_v_pmon
+; senr_c          :  ECategory senr_v_mon senr_c_obj senr_c_hom
+; senr_c_bin      :  EBinoidalCat senr_c
+; senr_c_i        :  senr_c
+; senr_c_pm       :  PreMonoidalCat senr_c_bin senr_c_i
 }.
 
 Definition SurjectiveEnrichmentToEnrichment (se:SurjectiveEnrichment) : Enrichment.
@@ -82,38 +92,19 @@ refine
 Defined.
 Coercion SurjectiveEnrichmentToEnrichment : SurjectiveEnrichment >-> Enrichment.
 
-(*
-Definition MonoidalEnrichment (e:Enrichment) :=
-  PreMonoidalFunctor
-    (enr_c_center_mon e)
-    (enr_v_pmon e)
-    (RestrictDomain (HomFunctor e (pmon_I (enr_c_pm e))) (Center (enr_c_pm e))).
-*)
 Definition MonoidalEnrichment (e:Enrichment) :=
   PreMonoidalFunctor
     (enr_c_pm e)
     (enr_v_pmon e)
     (HomFunctor e (pmon_I (enr_c_pm e))).
 
-
-(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
-(*
-Definition SurjectiveEnrichment (ec:Enrichment) :=
-  @treeDecomposition (enr_v ec) (option (ec*ec))
-                  (fun t => match t with
-                            | None   => enr_v_i ec
-                            | Some x => match x with pair y z => enr_c_hom ec y z end
-                            end)
-                  (enr_v_bobj ec).
-*)
-
 Class MonicEnrichment {e:Enrichment} :=
 { me_enr          := e
 ; me_homfunctor   := HomFunctor e (enr_c_i e)
-(*; me_homfunctor_c := RestrictDomain me_homfunctor (enr_c_center e)*)
 ; me_full         :  FullFunctor         me_homfunctor
 ; me_faithful     :  FaithfulFunctor     me_homfunctor
 ; me_conservative :  ConservativeFunctor me_homfunctor
+(*; me_homfunctor_c := RestrictDomain me_homfunctor (enr_c_center e)*)
 }.
 Implicit Arguments MonicEnrichment [ ].
 Coercion me_enr : MonicEnrichment >-> Enrichment.
@@ -122,7 +113,6 @@ Transparent HomFunctor.
 (* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
 Structure SMME :=
 { smme_e   : SurjectiveEnrichment
-(*; smme_see : SurjectiveEnrichment smme_e*)
 ; smme_mon : MonoidalEnrichment smme_e
 ; smme_mee : MonicEnrichment smme_e
 }.

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index f7f47a3..2f46f85 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -33,13 +33,9 @@ Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.
 Require Import HaskProofToStrong.
 
-Require Import ProgrammingLanguage.
-
 Require Import HaskProofFlattener.
 Require Import HaskProofStratified.
 
-Require Import ReificationsIsomorphicToGeneralizedArrows.
-
 Open Scope string_scope.
 Extraction Language Haskell.
 

diff --git a/src/GeneralizedArrow.v b/src/GeneralizedArrow.v
index 9149734..303baef 100644 (file)
--- a/src/GeneralizedArrow.v
+++ b/src/GeneralizedArrow.v
@@ -30,6 +30,12 @@ Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) :=
 { ga_functor_obj      : enr_v K -> ce
 ; ga_functor          : Functor            (enr_v_mon K) (enr_c_pm ce) ga_functor_obj
 ; ga_functor_monoidal : PreMonoidalFunctor (enr_v_mon K) (enr_c_pm ce) ga_functor
+
+(* We require that the host language (but NOT the guest language) be pure, i.e. all morphisms central, to simplify
+ * things.  If this doesn't suit you, just consider the "host language" here to be the pure sublanguage of the
+ * host language, and toss on the inclusion functor to the full language *)
+; ga_host_lang_pure   : CommutativeCat (enr_c_pm ce)
+
 (*
 ; ga_functor          : Functor         (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor_obj
 ; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor

diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v
index 3a6a74a..745484b 100644 (file)
--- a/src/GeneralizedArrowCategory.v
+++ b/src/GeneralizedArrowCategory.v
@@ -62,6 +62,8 @@ Definition generalizedArrowOrIdentityFunc s1 s2 (f:GeneralizedArrowOrIdentity s1
 Instance compose_generalizedArrows (s0 s1 s2:SMMEs) 
   (g01:GeneralizedArrow s0 s1)(g12:GeneralizedArrow s1 s2) : GeneralizedArrow s0 s2 :=
     { ga_functor_monoidal := g01 >>⊗>> smme_mon s1 >>⊗>> g12 }.
+  apply ga_host_lang_pure.
+  Defined.
 
 Definition generalizedArrowOrIdentityComp
   : forall s1 s2 s3, GeneralizedArrowOrIdentity s1 s2 -> GeneralizedArrowOrIdentity s2 s3 -> GeneralizedArrowOrIdentity s1 s3.

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 810e862..df6ef76 100644 (file)
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -265,13 +265,230 @@ Section GArrowFromReification.
        (garrow_functor >>>> bin_second(BinoidalCat:=enr_c_bin C) (R' a))
     <~~~>  (bin_second(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) :=
     { ni_iso := fun a => iso_id _ }.
-    admit.
+    intros.
+      etransitivity.  apply iso_id_lemma1.  symmetry.
+      etransitivity.  apply iso_id_lemma2.  symmetry.
+
+    Opaque Underlying.
+    unfold garrow_functor.
+      unfold functor_comp at 1.
+      unfold functor_comp at 1.
+      Opaque functor_comp. simpl. Transparent functor_comp.
+
+    symmetry.
+      eapply transitivity.
+      apply (functor_comp_assoc (RestrictToImage reification) (R' >>>> step2_functor) (ebc_second (R' a)) f).
+      unfold functor_comp at 1.
+      unfold functor_comp at 1.
+      Opaque functor_comp. simpl. Transparent functor_comp.
+
+    symmetry.
+      eapply transitivity.
+      set (ni_commutes (mf_second(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq.
+      unfold functor_comp in qq.
+      simpl in qq.
+      apply iso_shift_right' in qq.
+      apply (fmor_respects(R' >>>> step2_functor) _ _ qq).
+
+    apply (me_faithful(MonicEnrichment:=CMon)).
+      symmetry.
+      unfold fmor at 1.
+      eapply transitivity.
+      set (ni_commutes (mf_second(PreMonoidalFunctor:=CM) (R' a))) as zz.
+      unfold functor_comp in zz; unfold functor_fobj in zz; simpl in zz.
+      set (zz _ _ ((R' >>>> step2_functor) \ (reification \ f))) as zz'.
+      apply iso_shift_right' in zz'.
+      apply zz'.
+
+    unfold functor_comp; simpl.
+
+    symmetry.
+      eapply transitivity.
+      set full_roundtrip as full_roundtrip'.
+      unfold fmor in full_roundtrip'.
+      simpl in full_roundtrip'.
+      apply full_roundtrip'.
+
+    set (@iso_shift_right') as q. simpl in q. apply q. clear q.
+
+    set (@iso_shift_left) as q.   simpl in q. apply q. clear q.
+
+    symmetry.
+      eapply transitivity.
+      set full_roundtrip as full_roundtrip'.
+      unfold fmor in full_roundtrip'.
+      simpl in full_roundtrip'.
+      apply (fun a' b' f z => fmor_respects (bin_second(BinoidalCat:=enr_v_bin C) z) _ _ (full_roundtrip' a' b' f)).
+      symmetry.
+
+    intros.
+      unfold bin_obj.
+      unfold senr_v_bobj.
+
+    setoid_rewrite <- associativity.
+      setoid_rewrite <- associativity.
+      setoid_rewrite <- associativity.
+      setoid_rewrite <- associativity.
+      simpl.
+      setoid_rewrite <- associativity.
+      etransitivity.
+      eapply transitivity.
+        apply associativity.
+        eapply transitivity; [ idtac | apply right_identity ].
+        apply comp_respects; [ reflexivity | idtac ].
+        etransitivity.
+        apply comp_respects; [ idtac | reflexivity ].
+        apply (mf_consistent(PreMonoidalFunctor:=CM)).
+        apply iso_comp1.
+
+    eapply transitivity.
+      eapply comp_respects; [ idtac | reflexivity ].
+      eapply comp_respects; [ idtac | reflexivity ].
+      eapply comp_respects; [ idtac | reflexivity ].
+      eapply comp_respects; [ idtac | reflexivity ].
+      eapply transitivity.
+        eapply symmetry.
+        eapply associativity.
+      eapply transitivity; [ idtac | apply left_identity ].
+      eapply comp_respects; [ idtac | reflexivity ].
+      eapply transitivity.
+        eapply comp_respects; [ idtac | reflexivity ].
+        eapply symmetry.
+        apply (mf_consistent(PreMonoidalFunctor:=CM)).
+        apply iso_comp1.
+
+    eapply symmetry.
+      eapply transitivity.
+      setoid_rewrite <- fmor_preserves_comp.
+      setoid_rewrite <- fmor_preserves_comp.
+      eapply reflexivity.
+      eapply symmetry.
+
+    apply comp_respects; try reflexivity.
+
+    eapply transitivity.
+      apply associativity.
+      eapply transitivity.
+      apply associativity.
+      eapply transitivity.
+      apply associativity.
+      eapply transitivity.
+      apply associativity.
+      apply comp_respects; try reflexivity.
+
+    eapply transitivity.
+      eapply comp_respects; [ reflexivity | idtac ].
+      eapply transitivity.
+      eapply comp_respects; [ idtac | reflexivity ].
+      apply mf_consistent.
+      eapply transitivity.
+      eapply comp_respects; [ reflexivity | idtac ].
+        apply associativity.
+      apply iso_comp1_right.
+
+    eapply transitivity.
+      eapply comp_respects; [ reflexivity | idtac ].
+      eapply transitivity.
+        apply associativity.
+      eapply comp_respects; [ reflexivity | idtac ].
+      eapply transitivity.
+        eapply symmetry.
+        apply associativity.
+      eapply transitivity; [ idtac | apply left_identity ].
+      eapply comp_respects; [ idtac | reflexivity ].
+      eapply transitivity.
+        eapply comp_respects; [ idtac | reflexivity ].
+        eapply symmetry.
+        eapply (mf_consistent(PreMonoidalFunctor:=reification)).
+      apply iso_comp1.
+
+    eapply transitivity.
+      eapply comp_respects; [ reflexivity | idtac ].
+      eapply symmetry.
+      apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+      eapply transitivity; [ idtac | apply right_identity ].
+
+    eapply transitivity.
+      eapply symmetry.
+      apply associativity.
+    eapply transitivity.
+      eapply comp_respects; [ idtac | reflexivity ].
+      unfold functor_fobj.
+      apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
+
+    apply symmetry.
+      eapply transitivity.
+      apply right_identity.
+      apply symmetry.
+      eapply transitivity; [ idtac | apply left_identity ].
+      apply comp_respects; [ idtac | reflexivity ].
+
+    eapply transitivity.
+      Focus 2.
+      eapply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
+      idtac.
+      apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
+      apply iso_comp2.
     Defined.
 
 Implicit Arguments mf_first [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
 Implicit Arguments mf_second [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
 Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
 
+  Lemma assoc_coherent (a b c : enr_v K) :
+   (#((pmon_assoc(PreMonoidalCat:=enr_c_pm C)
+     (garrow_functor a) (garrow_functor c)) (garrow_fobj b)) >>> garrow_functor a ⋊ #((garrow_first c) b)) >>>
+   #((garrow_second a) (b ⊗ c)) ~~
+   (#((garrow_second a) b) ⋉ garrow_functor c >>>
+     #((garrow_first c) (a ⊗ b))) >>> garrow_functor \ #((pmon_assoc(PreMonoidalCat:=enr_v_mon K) a c) b).
+    Opaque Underlying.
+    eapply transitivity.
+      eapply transitivity; [ idtac | apply right_identity ].
+      eapply comp_respects; [ eapply reflexivity | idtac ].
+      reflexivity.
+
+    apply symmetry.
+      eapply transitivity.
+      eapply transitivity; [ idtac | apply left_identity ].
+      eapply comp_respects; [ idtac | eapply reflexivity ].
+      eapply transitivity; [ idtac | apply right_identity ].
+      apply comp_respects.
+      simpl.
+      apply (fmor_preserves_id (ebc_first (garrow_functor c))).
+      reflexivity.
+
+    symmetry.
+      eapply transitivity.
+      eapply transitivity; [ idtac | apply right_identity ].
+      apply comp_respects. 
+      reflexivity.
+      simpl.
+      apply (fmor_preserves_id (ebc_second (garrow_functor a))).
+      symmetry.
+
+    unfold functor_fobj.
+      unfold garrow_functor.
+      unfold step2_functor.
+      Opaque R'.
+      Opaque ff_functor_section_functor.
+      unfold functor_comp.
+      simpl.
+      Transparent R'.
+      Transparent ff_functor_section_functor.
+      idtac.
+      apply (me_faithful(MonicEnrichment:=CMon)).
+      eapply transitivity; [ eapply full_roundtrip | idtac ].
+
+    unfold fmor at 1.
+      unfold R'.
+      unfold me_homfunctor.
+      set (mf_assoc(PreMonoidalFunctor:=reification) a b c) as q.
+      set (mf_assoc(PreMonoidalFunctor:=CM) (garrow_fobj a) (garrow_fobj b) (garrow_fobj c)) as q'.
+      unfold mf_F in q'.
+      unfold pmon_I in q'.
+      admit.
+      Qed.
+
   Lemma cancell_lemma `(F:PreMonoidalFunctor) b :
     iso_backward (mf_i F) ⋉ (F b) >>> #(pmon_cancell (F b)) ~~
     #((mf_first F b) _) >>>  F \ #(pmon_cancell b).
@@ -428,7 +645,6 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0]
    #(pmon_cancelr(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
    (garrow_functor b ⋊ #(iso_id (enr_c_i C)) >>>
     #((garrow_second b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancelr(PreMonoidalCat:=enr_v_mon K) b).
-
     Opaque Underlying.
     Opaque fmor.
     intros; simpl.
@@ -534,21 +750,16 @@ Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0]
   ; mf_second     := garrow_second
   ; mf_i          := iso_id _ }.
     intros; reflexivity.
-    intros.
-      unfold garrow_functor.
-      unfold fmor.
-      Opaque fmor. simpl.
-      unfold step2_functor.
-      admit.
-      Transparent fmor.
-
+    intros; apply (reification_host_lang_pure _ _ _ reification).
     apply cancell_coherent.
     apply cancelr_coherent.
-    admit.
+    apply assoc_coherent.
     Defined.
 
   Definition garrow_from_reification : GeneralizedArrow K CM :=
-    {| ga_functor_monoidal := garrow_monoidal |}.
+    {| ga_functor_monoidal := garrow_monoidal
+     ; ga_host_lang_pure   := reification_host_lang_pure _ _ _ reification
+    |}.
 
 End GArrowFromReification.
 

diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v
index 82bc678..fcc2a37 100644 (file)
--- a/src/HaskProofFlattener.v
+++ b/src/HaskProofFlattener.v
@@ -133,6 +133,7 @@ Section HaskProofFlattener.
    * it might help to have the definition for "Inductive ND" (see
    * NaturalDeduction.v) handy as a cross-reference.
    *)
+(*
   Definition FlatteningFunctor_fmor {Γ}{Δ}{ec}
     : forall h c,
       (h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) ->
@@ -392,6 +393,6 @@ Section HaskProofFlattener.
       *)
 
   (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
-
+*)
 End HaskProofFlattener.
 

diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v
index 1f7d85d..5c5f68a 100644 (file)
--- a/src/HaskProofStratified.v
+++ b/src/HaskProofStratified.v
@@ -441,9 +441,9 @@ Section HaskProofStratified.
   Instance OrgPCF_ContextND_Relation Γ Δ lev : ContextND_Relation (PCF_sequent_join Γ Δ lev).
     admit.
     Defined.
-
+(*
   (* 5.1.3 *)
-  Instance PCF Γ Δ lev : @ProgrammingLanguage _ _ pcfjudg (PCFRule Γ Δ lev) :=
+  Instance PCF Γ Δ lev : @ProgrammingLanguage _ pcfjudg (PCFRule Γ Δ lev) :=
   { pl_eqv                := OrgPCF_ContextND_Relation Γ Δ lev
   ; pl_snd                := PCF_sequents Γ Δ lev
   }.
@@ -571,5 +571,5 @@ Section HaskProofStratified.
 *)
 admit.
     Defined.
-
+*)
 End HaskProofStratified.

diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v
index 7ac59b3..d721a97 100644 (file)
--- a/src/NaturalDeductionCategory.v
+++ b/src/NaturalDeductionCategory.v
@@ -72,7 +72,7 @@ Section Judgments_Category.
       setoid_rewrite <- ndr_prod_preserves_comp.
       apply (ndr_builtfrom_structural (f;;g)); auto.
     Defined.
-  Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (fun x y => x,,y) :=
+  Instance Judgments_Category_binoidal : BinoidalCat Judgments_Category (@T_Branch (??Judgment)) :=
     { bin_first  := jud_first
     ; bin_second := jud_second }.
 

diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v
index 933785a..7ac2af7 100644 (file)
--- a/src/ProgrammingLanguage.v
+++ b/src/ProgrammingLanguage.v
@@ -34,11 +34,11 @@ Section Programming_Language.
 
   Context {T    : Type}.               (* types of the language *)
 
-  Context (Judg : Type).
-  Context (sequent : Tree ??T -> Tree ??T -> Judg).
+  Definition PLJudg := (Tree ??T) * (Tree ??T).
+  Definition sequent := @pair (Tree ??T) (Tree ??T).
      Notation "cs |= ss" := (sequent cs ss) : pl_scope.
 
-  Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}.
+  Context {Rule : Tree ??PLJudg -> Tree ??PLJudg -> Type}.
 
   Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
 
@@ -47,11 +47,11 @@ Section Programming_Language.
   Open Scope pl_scope.
 
   Class ProgrammingLanguage :=
-  { pl_eqv0               :  @ND_Relation Judg Rule
-  ; pl_snd                :> @SequentND Judg Rule _ sequent
-  ; pl_cnd                :> @ContextND Judg Rule T sequent pl_snd
-  ; pl_eqv1               :> @SequentND_Relation Judg Rule _ sequent pl_snd pl_eqv0
-  ; pl_eqv                :> @ContextND_Relation Judg Rule _ sequent pl_snd pl_cnd pl_eqv0 pl_eqv1
+  { pl_eqv0               :  @ND_Relation PLJudg Rule
+  ; pl_snd                :> @SequentND PLJudg Rule _ sequent
+  ; pl_cnd                :> @ContextND PLJudg Rule T sequent pl_snd
+  ; pl_eqv1               :> @SequentND_Relation PLJudg Rule _ sequent pl_snd pl_eqv0
+  ; pl_eqv                :> @ContextND_Relation PLJudg Rule _ sequent pl_snd pl_cnd pl_eqv0 pl_eqv1
   }.
   Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3.
 
@@ -171,8 +171,21 @@ Section Programming_Language.
 
     Instance Types_assoc a b : Types_second a >>>> Types_first b <~~~> Types_first b >>>> Types_second a :=
       { ni_iso := fun c => Types_assoc_iso a c b }.
-      intros; unfold eqv; simpl.
-      admit.
+(*
+      intros. unfold functor_comp. unfold fmor.
+      Opaque Types_assoc_iso.
+      simpl.
+      
+      eapply cndr_inert.
+      apply pl_eqv.
+      apply ndpc_comp; auto.
+      apply ndpc_comp; auto.
+      apply ndpc_comp; auto.
+      apply ndpc_prod; auto.
+      apply ndpc_comp; auto.
+      apply ndpc_comp; auto.
+*)
+admit.
       Defined.
 
     Instance Types_cancelr   : Types_first [] <~~~> functor_id _ :=
@@ -196,7 +209,7 @@ Section Programming_Language.
       admit.
       Defined.
 
-    Instance Types_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
+    Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
       { pmon_assoc    := Types_assoc
       ; pmon_cancell  := Types_cancell
       ; pmon_cancelr  := Types_cancelr
@@ -251,44 +264,19 @@ admit.
       admit.  (* cancell central *)
       Defined.
 
-    Definition TypesEnrichedInJudgments : Enrichment.
+    Definition TypesEnrichedInJudgments : SurjectiveEnrichment.
       refine
-        {| enr_v_mon := Judgments_Category_monoidal _
-         ; enr_c_pm  := Types_PreMonoidal
-         ; enr_c_bin := Types_binoidal
+        {| senr_c_pm     := TypesL_PreMonoidal
+         ; senr_v        := JudgmentsL
+         ; senr_v_bin    := Judgments_Category_binoidal _
+         ; senr_v_pmon   := Judgments_Category_premonoidal _
+         ; senr_v_mon    := Judgments_Category_monoidal _
+         ; senr_c_bin    := Types_binoidal
+         ; senr_c        := TypesL
         |}.
       Defined.
 
-    Structure HasProductTypes :=
-    {
-    }.
-
-    (*
-    Lemma CartesianEnrMonoidal (e:PreMonoidalEnrichment)
-      `(C:CartesianCat(Ob:= _)(Hom:= _)(C:=Underlying (enr_c e))) : MonoidalEnrichment e.
-      admit.
-      Defined.
-      *)
-
-    (* need to prove that if we have cartesian tuples we have cartesian contexts *)
-    (*
-    Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
-      admit.
-      Defined.
-      *)
   End LanguageCategory.
 
 End Programming_Language.
-(*
-Structure ProgrammingLanguageSMME :=
-{ plsmme_t       : Type
-; plsmme_judg    : Type
-; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg
-; plsmme_rule    : Tree ??plsmme_judg -> Tree ??plsmme_judg -> Type
-; plsmme_pl      : @ProgrammingLanguage plsmme_t plsmme_judg plsmme_sequent plsmme_rule
-; plsmme_smme    : SurjectiveMonicMonoidalEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl)
-}.
-Coercion plsmme_pl   : ProgrammingLanguageSMME >-> ProgrammingLanguage.
-Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
-*) 
 Implicit Arguments ND [ Judgment ].

diff --git a/src/ProgrammingLanguageArrow.v b/src/ProgrammingLanguageArrow.v
index b613455..f6a3940 100644 (file)
--- a/src/ProgrammingLanguageArrow.v
+++ b/src/ProgrammingLanguageArrow.v
@@ -18,6 +18,9 @@ Require Import Enrichment_ch2_8.
 Require Import Subcategories_ch7_1.
 Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
+Require Import PreMonoidalCenter.
 Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
 Require Import Enrichment_ch2_8.
@@ -41,35 +44,28 @@ Section ArrowInLanguage.
   Context `(Host:ProgrammingLanguage).
 
   (* ... for which Types(L) is cartesian: *)
-  Context {MF}(center_of_TypesL:MonoidalCat (TypesL _ _ Host) (fun x => (fst_obj _ _ x),,(snd_obj _ _ x)) MF []).
+  Context (center_of_TypesL:MonoidalCat (TypesL_PreMonoidal Host)).
 
-  (* along with a monoidal subcategory of Z(Types(L)) *)
-  Context (VK:MonoidalSubCat center_of_TypesL).
+  (* along with a full subcategory of Z(Types(L)) *)
+  Context {P}(VK:FullSubcategory (Center (TypesL_PreMonoidal Host)) P).
 
-  (* a premonoidal category enriched in aforementioned full subcategory *)
-  Context (Kehom:center_of_TypesL -> center_of_TypesL -> @ob _ _ VK).
-
-  Context (KE:@ECategory (@ob _ _ VK) (@hom _ _ VK) VK _ VK
-               (mon_i (full_subcat_is_monoidal VK)) (full_subcat_is_monoidal VK) center_of_TypesL Kehom).
-
-  Context {kbo:center_of_TypesL -> center_of_TypesL -> center_of_TypesL}.
+  Context (Pobj_unit   : P []).
+  Context (Pobj_closed : forall a b, P a → P b → P (bin_obj(BinoidalCat:=Center_is_PreMonoidal (TypesL_PreMonoidal Host)) a b)).
+  Definition VKM :=
+    PreMonoidalFullSubcategory_PreMonoidal (Center_is_PreMonoidal (TypesL_PreMonoidal Host)) VK Pobj_unit Pobj_closed.
 
-  Context (kbc:@BinoidalCat center_of_TypesL _ (Underlying KE) kbo).
+  (* a premonoidal category enriched in aforementioned full subcategory *)
+  Context (Kehom:(Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host)) -> @ob _ _ VK).
+  Context (KE   :@ECategory (@ob _ _ VK) (@hom _ _ VK) VK _ VKM (pmon_I VKM) VKM (Center (TypesL_PreMonoidal Host)) Kehom).
+  Context {kbo  :(Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host)) -> (Center (TypesL_PreMonoidal Host))}.
+  Context (kbc  :@BinoidalCat (Center (TypesL_PreMonoidal Host)) _ (Underlying KE) kbo).
 
-  Check (@PreMonoidalCat)
   Definition one' := @one _ _ _ (car_terminal(CartesianCat:=CC))
-  Context (K:@PreMonoidalCat _ _ KE kbo kbc ).
-  Context (CC:CartesianCat center_of_TypesL).
-
-  (*
-  Definition K_enrichment : Enrichment.
-    refine {| enr_c := KE |}.
-    Defined.
-  Context (K_surjective:SurjectiveEnrichment K_enrichment).
-    *)
+  Context (K :@PreMonoidalCat _ _ KE kbo kbc ).
+  Context (CC:CartesianCat (Center (TypesL_PreMonoidal Host))).
 
   Definition ArrowInProgrammingLanguage :=
-    @FreydCategory _ _ _ _ _ _ center_of_TypesL _ _ _ _ K.
+    @FreydCategory _ _ _ _ _ _ (Center (TypesL_PreMonoidal Host)) _ _ _ _ K.
 
   Definition ArrowsAreGeneralizedArrows (arrow:ArrowInProgrammingLanguage) : GeneralizedArrow K_enrichment Host.
     refine {| ga_functor_monoidal := inclusion_functor_monoidal VK |}.

diff --git a/src/ProgrammingLanguageGeneralizedArrow.v b/src/ProgrammingLanguageGeneralizedArrow.v
index bac2397..bed54b6 100644 (file)
--- a/src/ProgrammingLanguageGeneralizedArrow.v
+++ b/src/ProgrammingLanguageGeneralizedArrow.v
@@ -27,22 +27,21 @@ Require Import FunctorCategories_ch7_7.
 Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 
-Require Import FreydCategories.
-
+Require Import Enrichments.
 Require Import Reification.
 Require Import GeneralizedArrow.
-Require Import GeneralizedArrowFromReification.
 Require Import ProgrammingLanguage.
 
-Require Import ReificationsAndGeneralizedArrows.
-Require Import ReificationFromGeneralizedArrow.
-
 Section ProgrammingLanguageGeneralizedArrow.
 
-  Context (Guest:ProgrammingLanguageSMME) (Host :ProgrammingLanguageSMME).
+  Context
+  `(Guest        : ProgrammingLanguage)
+  `(Host         : ProgrammingLanguage)
+   (HostMonoidal : MonoidalEnrichment (TypesEnrichedInJudgments Host))
+   (HostMonic    : MonicEnrichment    (TypesEnrichedInJudgments Host)).
 
   Definition GeneralizedArrowInLanguage 
-    := GeneralizedArrow Guest Host.
+    := GeneralizedArrow (TypesEnrichedInJudgments Guest) HostMonoidal.
 
 End ProgrammingLanguageGeneralizedArrow.
 

diff --git a/src/ProgrammingLanguageReification.v b/src/ProgrammingLanguageReification.v
index ab8bb90..f6a2a8e 100644 (file)
--- a/src/ProgrammingLanguageReification.v
+++ b/src/ProgrammingLanguageReification.v
@@ -29,6 +29,25 @@ Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 Require Import ProgrammingLanguage.
 
+(*
+  Structure ProgrammingLanguageSMME :=
+  { plsmme_t       : Type
+  ; plsmme_judg    : Type
+  ; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg
+  ; plsmme_rule    : Tree ??plsmme_judg -> Tree ??plsmme_judg -> Type
+  ; plsmme_pl      : @ProgrammingLanguage plsmme_t plsmme_judg plsmme_sequent plsmme_rule
+  ; plsmme_smme    : SurjectiveEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl)
+  }.
+  Coercion plsmme_pl   : ProgrammingLanguageSMME >-> ProgrammingLanguage.
+  Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
+*)
+
+  Context
+  `(Guest        : ProgrammingLanguage)
+  `(Host         : ProgrammingLanguage)
+   (HostMonoidal : MonoidalEnrichment (TypesEnrichedInJudgments Host))
+   (HostMonic    : MonicEnrichment    (TypesEnrichedInJudgments Host)).
+
 Definition TwoLevelLanguage (Guest Host:ProgrammingLanguageSMME)
   := Reification Guest Host (me_i Host).
 

diff --git a/src/Reification.v b/src/Reification.v
index 932d78e..0daca47 100644 (file)
--- a/src/Reification.v
+++ b/src/Reification.v
@@ -35,6 +35,11 @@ Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) :=
 ; reification_rstar_f   :             Functor (enr_v K) (enr_v C) reification_rstar_obj
 ; reification_rstar     :             PreMonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
 ; reification_commutes  : ∀ k, reification_r k >>>> HomFunctor C CI <~~~> HomFunctor K k >>>> reification_rstar_f
+
+(* We require that the host language (but NOT the guest language) be pure, i.e. all morphisms central, to simplify
+ * things.  If this doesn't suit you, just consider the "host language" here to be the pure sublanguage of the
+ * host language, and toss on the inclusion functor to the full language *)
+; reification_host_lang_pure   : CommutativeCat (enr_c_pm C)
 }.
 Transparent HomFunctor.
 Transparent functor_comp.

diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
index 9a7c3fd..2261f88 100644 (file)
--- a/src/ReificationCategory.v
+++ b/src/ReificationCategory.v
@@ -97,6 +97,7 @@ Definition compose_reifications (s0 s1 s2:SMMEs) :
   apply (ni_respects2 (a >>>> a') (b >>>> b') x).
   apply ni_inv.
   apply comm1.
+  apply (reification_host_lang_pure _ _ _ X0).
   Defined.
 
 Definition reificationOrIdentityComp

diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v
index 2a9937f..1a5fea7 100644 (file)
--- a/src/ReificationFromGeneralizedArrow.v
+++ b/src/ReificationFromGeneralizedArrow.v
@@ -34,6 +34,7 @@ Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce)
    ; reification_rstar     := PreMonoidalFunctorsCompose garrow C
    |}.
    abstract (intros; set (@ni_associativity) as q; apply q).
+   intros; apply ga_host_lang_pure.
    Defined.