clean up hints for NaturalDeduction, split ProgrammingLanguage into multiple files

diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v
index 719e714..3aeb7db 100644 (file)
--- a/src/NaturalDeduction.v
+++ b/src/NaturalDeduction.v
@@ -229,18 +229,7 @@ Section Natural_Deduction.
   Hint Constructors Structural.
   Hint Constructors BuiltFrom.
   Hint Constructors NDPredicateClosure.
-
-  Hint Extern 1 => apply nd_structural_id0.     
-  Hint Extern 1 => apply nd_structural_id1.     
-  Hint Extern 1 => apply nd_structural_cancell. 
-  Hint Extern 1 => apply nd_structural_cancelr. 
-  Hint Extern 1 => apply nd_structural_llecnac. 
-  Hint Extern 1 => apply nd_structural_rlecnac. 
-  Hint Extern 1 => apply nd_structural_assoc.   
-  Hint Extern 1 => apply nd_structural_cossa.   
-  Hint Extern 1 => apply ndpc_p.
-  Hint Extern 1 => apply ndpc_prod.
-  Hint Extern 1 => apply ndpc_comp.
+  Hint Unfold StructuralND.
 
   Lemma nd_id_structural : forall sl, StructuralND (nd_id sl).
     intros.
@@ -464,42 +453,6 @@ Coercion sndr_ndr  : SequentND_Relation >-> ND_Relation.
 Coercion cndr_sndr : ContextND_Relation >-> SequentND_Relation.
 
 Implicit Arguments ND [ Judgment ].
-Hint Constructors Structural.
-Hint Extern 1 => apply nd_id_structural.
-Hint Extern 1 => apply ndr_builtfrom_structural.
-Hint Extern 1 => apply nd_structural_id0.     
-Hint Extern 1 => apply nd_structural_id1.     
-Hint Extern 1 => apply nd_structural_cancell. 
-Hint Extern 1 => apply nd_structural_cancelr. 
-Hint Extern 1 => apply nd_structural_llecnac. 
-Hint Extern 1 => apply nd_structural_rlecnac. 
-Hint Extern 1 => apply nd_structural_assoc.   
-Hint Extern 1 => apply nd_structural_cossa.   
-Hint Extern 1 => apply ndpc_p.
-Hint Extern 1 => apply ndpc_prod.
-Hint Extern 1 => apply ndpc_comp.
-Hint Extern 1 => apply builtfrom_refl.
-Hint Extern 1 => apply builtfrom_prod1.
-Hint Extern 1 => apply builtfrom_prod2.
-Hint Extern 1 => apply builtfrom_comp1.
-Hint Extern 1 => apply builtfrom_comp2.
-Hint Extern 1 => apply builtfrom_P.
-
-Hint Extern 1 => apply snd_inert_initial.
-Hint Extern 1 => apply snd_inert_cut.
-Hint Extern 1 => apply snd_inert_structural.
-
-Hint Extern 1 => apply cnd_inert_initial.
-Hint Extern 1 => apply cnd_inert_cut.
-Hint Extern 1 => apply cnd_inert_structural.
-Hint Extern 1 => apply cnd_inert_cnd_ant_assoc.
-Hint Extern 1 => apply cnd_inert_cnd_ant_cossa.
-Hint Extern 1 => apply cnd_inert_cnd_ant_cancell.
-Hint Extern 1 => apply cnd_inert_cnd_ant_cancelr.
-Hint Extern 1 => apply cnd_inert_cnd_ant_llecnac.
-Hint Extern 1 => apply cnd_inert_cnd_ant_rlecnac.
-Hint Extern 1 => apply cnd_inert_se_expand_left.
-Hint Extern 1 => apply cnd_inert_se_expand_right.
 
 (* This first notation gets its own scope because it can be confusing when we're working with multiple different kinds
  * of proofs.  When only one kind of proof is in use, it's quite helpful though. *)
@@ -509,10 +462,39 @@ Notation "a ** b"   := (nd_prod a b)             : nd_scope.
 Notation "[# a #]"  := (nd_rule a)               : nd_scope.
 Notation "a === b"  := (@ndr_eqv _ _ _ _ _ a b)  : nd_scope.
 
+Hint Constructors Structural.
+Hint Constructors ND_Relation.
+Hint Constructors BuiltFrom.
+Hint Constructors NDPredicateClosure.
+Hint Constructors ContextND_Inert.
+Hint Constructors SequentND_Inert.
+Hint Unfold StructuralND.
+
 (* enable setoid rewriting *)
 Open Scope nd_scope.
 Open Scope pf_scope.
 
+Hint Extern 2 (StructuralND (nd_id _)) => apply nd_id_structural.
+Hint Extern 2 (NDPredicateClosure _ ( _ ;; _ ) ) => apply ndpc_comp.
+Hint Extern 2 (NDPredicateClosure _ ( _ ** _ ) ) => apply ndpc_prod.
+Hint Extern 2 (NDPredicateClosure (@Structural _ _) (nd_id _)) => apply nd_id_structural.
+Hint Extern 2 (BuiltFrom _ _ ( _ ;; _ ) ) => apply builtfrom_comp1.
+Hint Extern 2 (BuiltFrom _ _ ( _ ;; _ ) ) => apply builtfrom_comp2.
+Hint Extern 2 (BuiltFrom _ _ ( _ ** _ ) ) => apply builtfrom_prod1.
+Hint Extern 2 (BuiltFrom _ _ ( _ ** _ ) ) => apply builtfrom_prod2.
+
+(* Hint Constructors has failed me! *)
+Hint Extern 2 (@Structural _ _ _ _ (@nd_id0 _ _))         => apply nd_structural_id0.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_id1 _ _ _))       => apply nd_structural_id1.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_cancell _ _ _))   => apply nd_structural_cancell.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_cancelr _ _ _))   => apply nd_structural_cancelr.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_llecnac _ _ _))   => apply nd_structural_llecnac.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_rlecnac _ _ _))   => apply nd_structural_rlecnac.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_assoc _ _ _ _ _)) => apply nd_structural_assoc.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_cossa _ _ _ _ _)) => apply nd_structural_cossa.
+
+Hint Extern 4 (NDPredicateClosure _ _) => apply ndpc_p.
+
 Add Parametric Relation {jt rt ndr h c} : (h/⋯⋯/c) (@ndr_eqv jt rt ndr h c)
   reflexivity proved by  (@Equivalence_Reflexive  _ _ (ndr_eqv_equivalence h c))
   symmetry proved by     (@Equivalence_Symmetric  _ _ (ndr_eqv_equivalence h c))
@@ -534,7 +516,8 @@ Section ND_Relation_Facts.
 
   (* useful *)
   Lemma ndr_comp_right_identity : forall h c (f:h/⋯⋯/c), ndr_eqv (f ;; nd_id c) f.
-    intros; apply (ndr_builtfrom_structural f); auto.
+    intros; apply (ndr_builtfrom_structural f). auto.
+    auto.
     Defined.
 
   (* useful *)

diff --git a/src/NaturalDeductionCategory.v b/src/NaturalDeductionCategory.v
index d721a97..9360bfa 100644 (file)
--- a/src/NaturalDeductionCategory.v
+++ b/src/NaturalDeductionCategory.v
@@ -136,9 +136,9 @@ Section Judgments_Category.
   ; pmon_assoc_ll := jud_mon_assoc_ll
   }.
     unfold functor_fobj; unfold fmor; simpl;
-      apply Build_Pentagon; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto.
+      apply Build_Pentagon; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto 10.
     unfold functor_fobj; unfold fmor; simpl;
-      apply Build_Triangle; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto.
+      apply Build_Triangle; simpl; intros; apply (ndr_builtfrom_structural nd_id0); auto 10.
     intros; unfold eqv; simpl; auto; reflexivity.
     intros; unfold eqv; simpl; auto; reflexivity.
     intros; unfold eqv; simpl; apply Judgments_Category_Commutative.

diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v
index dc2256c..83b435a 100644 (file)
--- a/src/ProgrammingLanguage.v
+++ b/src/ProgrammingLanguage.v
@@ -26,9 +26,7 @@ Require Import Enrichment_ch2_8.
 Require Import RepresentableStructure_ch7_2.
 Require Import FunctorCategories_ch7_7.
 
-Require Import Enrichments.
 Require Import NaturalDeduction.
-Require Import NaturalDeductionCategory.
 
 Section Programming_Language.
 
@@ -47,687 +45,15 @@ Section Programming_Language.
   Open Scope pl_scope.
 
   Class ProgrammingLanguage :=
-  { pl_eqv0               :  @ND_Relation PLJudg Rule
+  { 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.
-
-  Section LanguageCategory.
-
-    Context (PL:ProgrammingLanguage).
-
-    (* category of judgments in a fixed type/coercion context *)
-    Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv.
-
-    Definition JudgmentsL          := Judgments_cartesian.
-
-    Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
-      unfold hom; simpl.
-      apply snd_initial.
-      Defined.
-
-    Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
-      unfold hom; simpl.
-      apply snd_cut.
-      Defined.
-
-    Existing Instance pl_eqv.
-
-    Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
-      refine
-      {| eid   := identityProof
-       ; ecomp := cutProof
-      |}; intros.
-      apply (mon_commutative(MonoidalCat:=JudgmentsL)).
-      apply (mon_commutative(MonoidalCat:=JudgmentsL)).
-      unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
-      unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
-      unfold identityProof; unfold cutProof; simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
-      apply ndpc_comp; auto.
-      apply ndpc_comp; auto.
-      Defined.
-
-    Instance Types_first c : EFunctor TypesL TypesL (fun x => x,,c ) :=
-      { efunc := fun x y => cnd_expand_right(ContextND:=pl_cnd) x y c }.
-      intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
-      intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
-      apply (cndr_inert pl_cnd); auto.
-      intros. unfold ehom. unfold comp. simpl. unfold cutProof.
-      rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (cnd_expand_right _ _ c) _ _ (nd_id1 (b|=c0))
-                  _ (nd_id1 (a,,c |= b,,c))  _ (cnd_expand_right _ _ c)).
-      setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [a,, c |= b,, c]).
-      setoid_rewrite (@ndr_comp_left_identity  _ _ pl_eqv [b |= c0]).
-      simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
-      Defined.
-
-    Instance Types_second c : EFunctor TypesL TypesL (fun x => c,,x) :=
-      { efunc := fun x y => ((@cnd_expand_left _ _ _ _ _ _ x y c)) }.
-      intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
-      intros. unfold ehom. unfold hom. unfold identityProof. unfold eid. simpl. unfold identityProof.
-      eapply cndr_inert; auto. apply pl_eqv.
-      intros. unfold ehom. unfold comp. simpl. unfold cutProof.
-      rewrite <- (@ndr_prod_preserves_comp _ _ pl_eqv _ _ (cnd_expand_left _ _ c) _ _ (nd_id1 (b|=c0))
-                  _ (nd_id1 (c,,a |= c,,b))  _ (cnd_expand_left _ _ c)).
-      setoid_rewrite (@ndr_comp_right_identity _ _ pl_eqv _ [c,,a |= c,,b]).
-      setoid_rewrite (@ndr_comp_left_identity  _ _ pl_eqv [b |= c0]).
-      simpl; eapply cndr_inert. apply pl_eqv. auto. auto.
-      Defined.
-
-    Definition Types_binoidal : EBinoidalCat TypesL (@T_Branch _).
-      refine
-        {| ebc_first  := Types_first
-         ; ebc_second := Types_second
-         |}.
-      Defined.
-
-    Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) :=
-      { iso_forward  := snd_initial _ ;; cnd_ant_cossa _ a b c
-      ; iso_backward := snd_initial _ ;; cnd_ant_assoc _ a b c
-      }.
-      simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        auto.
-      simpl; eapply cndr_inert. unfold identityProof; apply pl_eqv. auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        auto.
-        Defined.
-
-    Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a :=
-      { iso_forward  := snd_initial _ ;; cnd_ant_rlecnac _ a
-      ; iso_backward := snd_initial _ ;; cnd_ant_cancelr _ a
-      }.
-      unfold eqv; unfold comp; simpl.
-      eapply cndr_inert. apply pl_eqv. auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        auto.
-      unfold eqv; unfold comp; simpl.
-      eapply cndr_inert. apply pl_eqv. auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        auto.
-      Defined.
-
-    Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a :=
-      { iso_forward  := snd_initial _ ;; cnd_ant_llecnac _ a
-      ; iso_backward := snd_initial _ ;; cnd_ant_cancell _ a
-      }.
-      unfold eqv; unfold comp; simpl.
-      eapply cndr_inert. apply pl_eqv. auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        auto.
-      unfold eqv; unfold comp; simpl.
-      eapply cndr_inert. apply pl_eqv. auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        auto.
-      Defined.
-
-    (* this tactical searches the environment; setoid_rewrite doesn't seem to be able to do that properly sometimes *)
-    Ltac nd_swap_ltac P EQV :=
-      match goal with
-        [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] => 
-          set (@nd_swap _ _ EQV _ _ _ _ F G) as P
-      end.
-
-    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.
-      Opaque nd_id.
-      simpl.
-      Transparent nd_id.
-
-      rename A into X.
-      rename B into Y.
-      unfold ehom.
-      nd_swap_ltac p pl_eqv.
-      setoid_rewrite p.
-      clear p.
-
-      setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
-      setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
-      setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
-      setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
-
-      repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-      setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
-
-      set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q.
-      Opaque nd_id.
-      simpl in q.
-      setoid_rewrite <- q.
-
-      clear q.
-      set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q.      
-      simpl in q.
-      set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
-      set (isos_forward_equal_then_backward_equal _ _ q') as qq.
-      simpl in qq.
-      setoid_rewrite qq in q.
-      clear q' qq.
-      setoid_rewrite <- q.
-
-      setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-      apply ndr_comp_respects; try reflexivity.
-
-      Transparent nd_id.
-      apply (cndr_inert pl_cnd); auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        Defined.
-
-    Instance Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a :=
-      { ni_iso := fun c => Types_assoc_iso a b c }.
-      intros.
-      Opaque nd_id.
-      simpl.
-      Transparent nd_id.
-
-      rename A into X.
-      rename B into Y.
-      unfold ehom.
-      nd_swap_ltac p pl_eqv.
-      setoid_rewrite p.
-      clear p.
-
-      setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
-      setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
-      setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
-
-      repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-      setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
-
-      set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q.
-      Opaque nd_id.
-      simpl in q.
-      setoid_rewrite <- q.
-
-      clear q.
-      set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q.      
-      simpl in q.
-      set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
-      set (isos_forward_equal_then_backward_equal _ _ q') as qq.
-      simpl in qq.
-      setoid_rewrite qq in q.
-      clear q' qq.
-      setoid_rewrite <- q.
-
-      setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-      apply ndr_comp_respects; try reflexivity.
-
-      Transparent nd_id.
-      apply (cndr_inert pl_cnd); auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        Defined.
-
-    Instance Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b :=
-      { ni_iso := fun c => iso_inv _ _ (Types_assoc_iso c a b) }.
-      intros.
-      Opaque nd_id.
-      simpl.
-      Transparent nd_id.
-
-      rename A into X.
-      rename B into Y.
-      unfold ehom.
-      nd_swap_ltac p pl_eqv.
-      setoid_rewrite p.
-      clear p.
-
-      setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
-      setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
-      setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
-
-      repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-      setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
-
-      set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q.
-      Opaque nd_id.
-      simpl in q.
-      setoid_rewrite <- q.
-
-      clear q.
-      set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q.      
-      simpl in q.
-      set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
-      set (isos_forward_equal_then_backward_equal _ _ q') as qq.
-      simpl in qq.
-      setoid_rewrite qq in q.
-      clear q' qq.
-      setoid_rewrite <- q.
-
-      setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-      apply ndr_comp_respects; try reflexivity.
-
-      Transparent nd_id.
-      apply (cndr_inert pl_cnd); auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        Defined.
-
-    Instance Types_cancelr   : Types_first [] <~~~> functor_id _ :=
-      { ni_iso := Types_cancelr_iso }.
-      intros.
-      Opaque nd_id.
-      simpl.
-      unfold ehom.
-      nd_swap_ltac p pl_eqv.
-      setoid_rewrite p.
-      setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
-      repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-      setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
-
-      set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q.
-      Opaque nd_id.
-      simpl in q.
-      setoid_rewrite <- q.
-      clear q.
-
-      set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q.      
-      simpl in q.
-      set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
-      set (isos_forward_equal_then_backward_equal _ _ q') as qq.
-      simpl in qq.
-      setoid_rewrite qq in q.
-      clear q' qq.
-      setoid_rewrite <- q.
-
-      setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-      apply ndr_comp_respects; try reflexivity.
-      Transparent nd_id.
-      simpl.
-      apply (cndr_inert pl_cnd); auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-      Defined.
-
-    Instance Types_cancell   : Types_second [] <~~~> functor_id _ :=
-      { ni_iso := Types_cancell_iso }.
-      intros.
-      Opaque nd_id.
-      simpl.
-      unfold ehom.
-      nd_swap_ltac p pl_eqv.
-      setoid_rewrite p.
-      setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
-      repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-      setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
-
-      set (ni_commutes' (jud_mon_cancelr pl_eqv) f) as q.
-      Opaque nd_id.
-      simpl in q.
-      setoid_rewrite <- q.
-      clear q.
-
-      set (ni_commutes' (jud_mon_cancell pl_eqv) f) as q.      
-      simpl in q.
-      set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
-      set (isos_forward_equal_then_backward_equal _ _ q') as qq.
-      simpl in qq.
-      setoid_rewrite qq in q.
-      clear q' qq.
-      setoid_rewrite <- q.
-      setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-
-      apply ndr_comp_respects; try reflexivity.
-      Transparent nd_id.
-      simpl.
-      apply (cndr_inert pl_cnd); auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-        apply ndpc_comp; auto.
-      Defined.
-
-      Lemma TypesL_assoc_central a b c : CentralMorphism(H:=Types_binoidal) #((Types_assoc a b) c).
-      intros.
-        apply Build_CentralMorphism.
-        Opaque nd_id.
-        intros.
-        unfold bin_obj.
-        unfold ebc_bobj.
-        simpl.
-        unfold ehom.
-        nd_swap_ltac p pl_eqv.
-        setoid_rewrite p.
-        clear p.
-        setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
-        setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
-        repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-        setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
-
-        set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
-        Opaque nd_id.
-        simpl in q.
-        setoid_rewrite <- q.
-        clear q.
-
-        set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.      
-        simpl in q.
-        set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
-        set (isos_forward_equal_then_backward_equal _ _ q') as qq.
-        simpl in qq.
-        setoid_rewrite qq in q.
-        clear q' qq.
-        setoid_rewrite <- q.
-
-        setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-        apply ndr_comp_respects.
-        reflexivity.
-        
-        Transparent nd_id.
-        apply (cndr_inert pl_cnd); auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-
-        Opaque nd_id.
-        intros.
-        unfold bin_obj.
-        unfold ebc_bobj.
-        simpl.
-        unfold ehom.
-        symmetry.
-        nd_swap_ltac p pl_eqv.
-        setoid_rewrite p.
-        clear p.
-        setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
-        setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
-        repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-        setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
-
-        set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
-        Opaque nd_id.
-        simpl in q.
-        setoid_rewrite <- q.
-        clear q.
-
-        set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.      
-        simpl in q.
-        set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
-        set (isos_forward_equal_then_backward_equal _ _ q') as qq.
-        simpl in qq.
-        setoid_rewrite qq in q.
-        clear q' qq.
-        setoid_rewrite <- q.
-
-        setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-        apply ndr_comp_respects.
-        reflexivity.
-        
-        Transparent nd_id.
-        apply (cndr_inert pl_cnd); auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          Qed.
-
-      Lemma TypesL_cancell_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancell a).
-      intros.
-        apply Build_CentralMorphism.
-        Opaque nd_id.
-        intros.
-        unfold bin_obj.
-        unfold ebc_bobj.
-        simpl.
-        unfold ehom.
-        nd_swap_ltac p pl_eqv.
-        setoid_rewrite p.
-        clear p.
-        setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
-        setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
-        repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-        setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
-
-        set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
-        Opaque nd_id.
-        simpl in q.
-        setoid_rewrite <- q.
-        clear q.
-
-        set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.      
-        simpl in q.
-        set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
-        set (isos_forward_equal_then_backward_equal _ _ q') as qq.
-        simpl in qq.
-        setoid_rewrite qq in q.
-        clear q' qq.
-        setoid_rewrite <- q.
-
-        setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-        apply ndr_comp_respects.
-        reflexivity.
-        
-        Transparent nd_id.
-        apply (cndr_inert pl_cnd); auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-
-        Opaque nd_id.
-        intros.
-        unfold bin_obj.
-        unfold ebc_bobj.
-        simpl.
-        unfold ehom.
-        symmetry.
-        nd_swap_ltac p pl_eqv.
-        setoid_rewrite p.
-        clear p.
-        setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
-        setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
-        repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-        setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
-
-        set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
-        Opaque nd_id.
-        simpl in q.
-        setoid_rewrite <- q.
-        clear q.
-
-        set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.      
-        simpl in q.
-        set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
-        set (isos_forward_equal_then_backward_equal _ _ q') as qq.
-        simpl in qq.
-        setoid_rewrite qq in q.
-        clear q' qq.
-        setoid_rewrite <- q.
-
-        setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-        apply ndr_comp_respects.
-        reflexivity.
-        
-        Transparent nd_id.
-        apply (cndr_inert pl_cnd); auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          Qed.
-
-      Lemma TypesL_cancelr_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancelr a).
-      intros.
-        apply Build_CentralMorphism.
-        Opaque nd_id.
-        intros.
-        unfold bin_obj.
-        unfold ebc_bobj.
-        simpl.
-        unfold ehom.
-        nd_swap_ltac p pl_eqv.
-        setoid_rewrite p.
-        clear p.
-        setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
-        setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
-        repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-        setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
-
-        set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
-        Opaque nd_id.
-        simpl in q.
-        setoid_rewrite <- q.
-        clear q.
-
-        set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.      
-        simpl in q.
-        set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
-        set (isos_forward_equal_then_backward_equal _ _ q') as qq.
-        simpl in qq.
-        setoid_rewrite qq in q.
-        clear q' qq.
-        setoid_rewrite <- q.
-
-        setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-        apply ndr_comp_respects.
-        reflexivity.
-        
-        Transparent nd_id.
-        apply (cndr_inert pl_cnd); auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-
-        Opaque nd_id.
-        intros.
-        unfold bin_obj.
-        unfold ebc_bobj.
-        simpl.
-        unfold ehom.
-        symmetry.
-        nd_swap_ltac p pl_eqv.
-        setoid_rewrite p.
-        clear p.
-        setoid_rewrite (@nd_prod_split_left  _ Rule pl_eqv _ _ _ []).
-        setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
-        repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-        setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
-
-        set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
-        Opaque nd_id.
-        simpl in q.
-        setoid_rewrite <- q.
-        clear q.
-
-        set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.      
-        simpl in q.
-        set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
-        set (isos_forward_equal_then_backward_equal _ _ q') as qq.
-        simpl in qq.
-        setoid_rewrite qq in q.
-        clear q' qq.
-        setoid_rewrite <- q.
-
-        setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
-        apply ndr_comp_respects.
-        reflexivity.
-        
-        Transparent nd_id.
-        apply (cndr_inert pl_cnd); auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          apply ndpc_comp; auto.
-          Qed.
-
-    Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
-      { pmon_assoc    := Types_assoc
-      ; pmon_cancell  := Types_cancell
-      ; pmon_cancelr  := Types_cancelr
-      ; pmon_assoc_rr := Types_assoc_rr
-      ; pmon_assoc_ll := Types_assoc_ll
-      }.
-      apply Build_Pentagon.
-        intros; simpl.
-        eapply cndr_inert. apply pl_eqv.
-        apply ndpc_comp.
-        apply ndpc_comp.
-        auto.
-        apply ndpc_comp.
-        apply ndpc_prod.
-        apply ndpc_comp.
-        apply ndpc_comp.
-        auto.
-        apply ndpc_comp.
-        auto.
-        auto.
-        auto.
-        auto.
-        auto.
-        auto.
-        apply ndpc_comp.
-        apply ndpc_comp.
-        auto.
-        apply ndpc_comp.
-        auto.
-        auto.
-        auto.
-
-      apply Build_Triangle; intros; simpl.
-        eapply cndr_inert. apply pl_eqv.
-        auto.
-        apply ndpc_comp.
-        apply ndpc_comp.
-        auto.
-        apply ndpc_comp.
-        auto.
-        auto.
-        auto.
-        eapply cndr_inert. apply pl_eqv. auto.
-          auto.
-      intros; simpl; reflexivity.
-      intros; simpl; reflexivity.
-      apply TypesL_assoc_central.
-      apply TypesL_cancelr_central.
-      apply TypesL_cancell_central.
-      Defined.
-
-    Definition TypesEnrichedInJudgments : SurjectiveEnrichment.
-      refine
-        {| 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.
-
-  End LanguageCategory.
+  Coercion pl_eqv  : ProgrammingLanguage >-> ContextND_Relation.
+  Coercion pl_cnd  : ProgrammingLanguage >-> ContextND.
 
 End Programming_Language.
-Implicit Arguments ND [ Judgment ].
+

diff --git a/src/ProgrammingLanguageArrow.v b/src/ProgrammingLanguageArrow.v
index 5dbce6d..5386d3e 100644 (file)
--- a/src/ProgrammingLanguageArrow.v
+++ b/src/ProgrammingLanguageArrow.v
@@ -30,7 +30,7 @@ Require Import FunctorCategories_ch7_7.
 Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 
-Require Import ProgrammingLanguage.
+Require Import ProgrammingLanguageCategory.
 Require Import FreydCategories.
 Require Import Enrichments.
 Require Import GeneralizedArrow.

diff --git a/src/ProgrammingLanguageCategory.v b/src/ProgrammingLanguageCategory.v
new file mode 100644 (file)
index 0000000..d415a35
--- /dev/null
+++ b/src/ProgrammingLanguageCategory.v
@@ -0,0 +1,650 @@
+(*********************************************************************************************************************************)
+(* ProgrammingLanguageCategory                                                                                                   *)
+(*                                                                                                                               *)
+(*   The category Types(L)                                                                                                       *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Categories_ch1_3.
+Require Import InitialTerminal_ch2_2.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import OppositeCategories_ch1_6_2.
+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 MonoidalCategories_ch7_8.
+Require Import Coherence_ch7_8.
+Require Import Enrichment_ch2_8.
+Require Import RepresentableStructure_ch7_2.
+Require Import FunctorCategories_ch7_7.
+
+Require Import NaturalDeduction.
+Require Import ProgrammingLanguage.
+        Export ProgrammingLanguage.
+
+Require Import NaturalDeductionCategory.
+
+Open Scope nd_scope.
+(* I am at a loss to explain why "auto" can't handle this *)
+Ltac ndpc_tac :=
+  match goal with
+    | [ |- NDPredicateClosure ?P (?A ;; ?B) ] => apply ndpc_comp; ndpc_tac
+    | [ |- NDPredicateClosure ?P (?A ** ?B) ] => apply ndpc_prod; ndpc_tac
+    | _                                       => auto
+  end.
+
+(* this tactical searches the environment; setoid_rewrite doesn't seem to be able to do that properly sometimes *)
+Ltac nd_swap_ltac P EQV :=
+  match goal with
+    [ |- context [ (?F ** nd_id _) ;; (nd_id _ ** ?G) ] ] => 
+      set (@nd_swap _ _ EQV _ _ _ _ F G) as P
+  end.
+
+(* I still wish I knew why "Hint Constructors" doesn't work *)
+Hint Extern 5 => apply snd_inert_initial.
+Hint Extern 5 => apply snd_inert_cut.
+Hint Extern 5 => apply snd_inert_structural.
+Hint Extern 5 => apply cnd_inert_initial.
+Hint Extern 5 => apply cnd_inert_cut.
+Hint Extern 5 => apply cnd_inert_structural.
+Hint Extern 5 => apply cnd_inert_cnd_ant_assoc.
+Hint Extern 5 => apply cnd_inert_cnd_ant_cossa.
+Hint Extern 5 => apply cnd_inert_cnd_ant_cancell.
+Hint Extern 5 => apply cnd_inert_cnd_ant_cancelr.
+Hint Extern 5 => apply cnd_inert_cnd_ant_llecnac.
+Hint Extern 5 => apply cnd_inert_cnd_ant_rlecnac.
+Hint Extern 5 => apply cnd_inert_se_expand_left.
+Hint Extern 5 => apply cnd_inert_se_expand_right.
+
+Hint Extern 2 (@Structural _ _ _ _ (@nd_id _ _ []   )) => simpl; auto.
+Hint Extern 2 (@Structural _ _ _ _ (@nd_id _ _ [ _ ])) => simpl; auto.
+
+Section ProgrammingLanguageCategory.
+
+  Context {T    : Type}.               (* types of the language *)
+
+  Context {Rule : Tree ??(@PLJudg T) -> Tree ??(@PLJudg T) -> Type}.
+     Notation "cs |= ss" := (@sequent T cs ss) : pl_scope.
+
+  Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
+
+  Open Scope pf_scope.
+  Open Scope nd_scope.
+  Open Scope pl_scope.
+
+  Context (PL:@ProgrammingLanguage T Rule).
+
+  (* category of judgments in a fixed type/coercion context *)
+  Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule pl_eqv.
+
+  Definition JudgmentsL          := Judgments_cartesian.
+
+  Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
+    unfold hom; simpl.
+    apply snd_initial.
+    Defined.
+
+  Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
+    unfold hom; simpl.
+    apply snd_cut.
+    Defined.
+
+  Instance TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]) :=
+  { eid   := identityProof
+  ; ecomp := cutProof
+  }.
+    intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
+    intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
+    abstract (intros; unfold identityProof; unfold cutProof; simpl; eapply cndr_inert; auto; apply PL).
+    abstract (intros; unfold identityProof; unfold cutProof; simpl; eapply cndr_inert; auto; apply PL).
+    abstract (intros; unfold identityProof; unfold cutProof; simpl; eapply cndr_inert;
+                [ apply PL | idtac | idtac ]; apply ndpc_comp; auto).
+    Defined.
+
+  Instance Types_first c : EFunctor TypesL TypesL (fun x => x,,c ) :=
+    { efunc := fun x y => cnd_expand_right(ContextND:=pl_cnd) x y c }.
+    intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
+    abstract (intros; simpl; apply (cndr_inert pl_cnd); auto).
+    abstract (intros; unfold ehom; unfold comp; simpl; unfold cutProof;
+              rewrite <- (@ndr_prod_preserves_comp _ _ PL _ _ (cnd_expand_right _ _ c) _ _ (nd_id1 (b|=c0))
+                          _ (nd_id1 (a,,c |= b,,c))  _ (cnd_expand_right _ _ c));
+              setoid_rewrite (@ndr_comp_right_identity _ _ PL _ [a,, c |= b,, c]);
+              setoid_rewrite (@ndr_comp_left_identity  _ _ PL [b |= c0]);
+              simpl; eapply cndr_inert; [ apply PL | auto | auto ]).
+    Defined.
+
+  Instance Types_second c : EFunctor TypesL TypesL (fun x => c,,x) :=
+    { efunc := fun x y => ((@cnd_expand_left _ _ _ _ _ _ x y c)) }.
+    intros; apply (mon_commutative(MonoidalCat:=JudgmentsL)).
+    abstract (intros; simpl; apply (cndr_inert pl_cnd); auto).
+    intros; unfold ehom; unfold comp; simpl; unfold cutProof;
+    abstract (rewrite <- (@ndr_prod_preserves_comp _ _ PL _ _ (cnd_expand_left _ _ c) _ _ (nd_id1 (b|=c0))
+                          _ (nd_id1 (c,,a |= c,,b))  _ (cnd_expand_left _ _ c));
+              setoid_rewrite (@ndr_comp_right_identity _ _ PL _ [c,,a |= c,,b]);
+              setoid_rewrite (@ndr_comp_left_identity  _ _ PL [b |= c0]);
+              simpl; eapply cndr_inert; [ apply PL | auto | auto ]).
+    Defined.
+
+  Instance Types_binoidal : EBinoidalCat TypesL (@T_Branch _) :=
+  { ebc_first  := Types_first
+  ; ebc_second := Types_second
+  }.
+
+  Instance Types_assoc_iso a b c : Isomorphic(C:=TypesL) ((a,,b),,c) (a,,(b,,c)) :=
+  { iso_forward  := snd_initial _ ;; cnd_ant_cossa _ a b c
+  ; iso_backward := snd_initial _ ;; cnd_ant_assoc _ a b c
+  }.
+    abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
+    abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
+    Defined.
+
+  Instance Types_cancelr_iso a : Isomorphic(C:=TypesL) (a,,[]) a :=
+  { iso_forward  := snd_initial _ ;; cnd_ant_rlecnac _ a
+  ; iso_backward := snd_initial _ ;; cnd_ant_cancelr _ a
+  }.
+    abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
+    abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
+    Defined.
+
+  Instance Types_cancell_iso a : Isomorphic(C:=TypesL) ([],,a) a :=
+    { iso_forward  := snd_initial _ ;; cnd_ant_llecnac _ a
+    ; iso_backward := snd_initial _ ;; cnd_ant_cancell _ a
+    }.
+    abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
+    abstract (simpl; eapply cndr_inert; unfold identityProof; [ apply PL | idtac | idtac ]; ndpc_tac).
+    Defined.
+
+  Lemma coincide' : nd_llecnac === nd_rlecnac.
+    set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
+    set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+    apply qq.
+    Qed.
+
+  Lemma Types_assoc_lemma : ∀a b X Y : TypesL,
+      ∀f : X ~~{ TypesL }~~> Y,
+      #(Types_assoc_iso a X b) >>> (Types_first b >>>> Types_second a) \ f ~~
+      (Types_second a >>>> Types_first b) \ f >>> #(Types_assoc_iso a Y b).
+    intros.
+    Opaque nd_id.
+      simpl.
+      Transparent nd_id.
+    unfold ehom.
+
+    nd_swap_ltac p PL.
+      setoid_rewrite p.
+      clear p.
+
+    repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+
+    setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
+    setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
+    setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
+    setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
+
+    setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+    setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+    setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
+
+    set (ni_commutes' (jud_mon_cancelr PL) f) as q.
+      simpl in q.
+      setoid_rewrite <- q. 
+      clear q.
+
+    set (ni_commutes' (jud_mon_cancell PL) f) as q.      
+      simpl in q.
+      setoid_rewrite coincide' in q.
+      setoid_rewrite <- q.
+      clear q.
+
+    setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      apply ndr_comp_respects; try reflexivity.
+
+    apply (cndr_inert pl_cnd); auto; ndpc_tac; auto.
+    Qed.
+
+  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 }.
+    apply Types_assoc_lemma.
+    Defined.
+
+  Lemma Types_assoc_ll_lemma : 
+    ∀a b X Y : TypesL,
+    ∀f : X ~~{ TypesL }~~> Y,
+    #(Types_assoc_iso a b X) >>> (Types_second b >>>> Types_second a) \ f ~~
+    Types_second (a,, b) \ f >>> #(Types_assoc_iso a b Y).
+
+    intros.
+    Opaque nd_id.
+    simpl.
+    Transparent nd_id.
+    unfold ehom.
+    nd_swap_ltac p PL.
+    setoid_rewrite p.
+    clear p.
+
+    setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
+    setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
+    setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
+
+    repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+    setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
+
+    set (ni_commutes' (jud_mon_cancelr PL) f) as q.
+    Opaque nd_id.
+    simpl in q.
+    setoid_rewrite <- q.
+
+    clear q.
+    set (ni_commutes' (jud_mon_cancell PL) f) as q.      
+    simpl in q.
+    set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
+    set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+    simpl in qq.
+    setoid_rewrite qq in q.
+    clear q' qq.
+    setoid_rewrite <- q.
+
+    setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+    apply ndr_comp_respects; try reflexivity.
+
+    Transparent nd_id.
+    apply (cndr_inert pl_cnd); auto; ndpc_tac.
+    Qed.
+
+  Instance Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a :=
+    { ni_iso := fun c => Types_assoc_iso a b c }.
+    apply Types_assoc_ll_lemma.
+    Defined.
+
+  Lemma Types_assoc_rr_lemma :
+    ∀a b A B : TypesL,
+    ∀f : A ~~{ TypesL }~~> B,
+    #(Types_assoc_iso A a b) ⁻¹ >>> (Types_first a >>>> Types_first b) \ f ~~
+    Types_first (a,, b) \ f >>> #(Types_assoc_iso B a b) ⁻¹.
+    intros.
+    Opaque nd_id.
+    simpl.
+    Transparent nd_id.
+
+    rename A into X.
+    rename B into Y.
+    unfold ehom.
+    nd_swap_ltac p PL.
+    setoid_rewrite p.
+    clear p.
+
+    setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
+    setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
+    setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
+
+    repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+    setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
+
+    set (ni_commutes' (jud_mon_cancelr PL) f) as q.
+    Opaque nd_id.
+    simpl in q.
+    setoid_rewrite <- q.
+
+    clear q.
+    set (ni_commutes' (jud_mon_cancell PL) f) as q.      
+    simpl in q.
+    set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
+    set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+    simpl in qq.
+    setoid_rewrite qq in q.
+    clear q' qq.
+    setoid_rewrite <- q.
+
+    setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+    apply ndr_comp_respects; try reflexivity.
+
+    Transparent nd_id.
+    apply (cndr_inert pl_cnd); auto; ndpc_tac.
+    Qed.
+
+  Instance Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b :=
+    { ni_iso := fun c => iso_inv _ _ (Types_assoc_iso c a b) }.
+    apply Types_assoc_rr_lemma.
+    Defined.
+
+  Lemma Types_cancelr_lemma :
+    ∀A B : TypesL,
+    ∀f : A ~~{ TypesL }~~> B,
+    #(Types_cancelr_iso A) >>> functor_id TypesL \ f ~~
+    Types_first [] \ f >>> #(Types_cancelr_iso B).
+    intros.
+    Opaque nd_id.
+    simpl.
+    unfold ehom.
+    nd_swap_ltac p PL.
+    setoid_rewrite p.
+    setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
+    repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+    setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
+
+    set (ni_commutes' (jud_mon_cancelr PL) f) as q.
+    Opaque nd_id.
+    simpl in q.
+    setoid_rewrite <- q.
+    clear q.
+
+    set (ni_commutes' (jud_mon_cancell PL) f) as q.      
+    simpl in q.
+    set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
+    set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+    simpl in qq.
+    setoid_rewrite qq in q.
+    clear q' qq.
+    setoid_rewrite <- q.
+
+    setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+    apply ndr_comp_respects; try reflexivity.
+    Transparent nd_id.
+    simpl.
+    apply (cndr_inert pl_cnd); auto; ndpc_tac.
+    Qed.
+
+  Instance Types_cancelr   : Types_first [] <~~~> functor_id _ :=
+    { ni_iso := Types_cancelr_iso }.
+    apply Types_cancelr_lemma.
+    Defined.
+
+  Lemma Types_cancell_lemma :
+    ∀A B : TypesL,
+    ∀f : A ~~{ TypesL }~~> B,
+    #(Types_cancell_iso A) >>> functor_id TypesL \ f ~~
+    Types_second [] \ f >>> #(Types_cancell_iso B).
+    intros.
+    Opaque nd_id.
+    simpl.
+    unfold ehom.
+    nd_swap_ltac p PL.
+    setoid_rewrite p.
+    setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
+    repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+    setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
+
+    set (ni_commutes' (jud_mon_cancelr PL) f) as q.
+    Opaque nd_id.
+    simpl in q.
+    setoid_rewrite <- q.
+    clear q.
+
+    set (ni_commutes' (jud_mon_cancell PL) f) as q.      
+    simpl in q.
+    set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
+    set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+    simpl in qq.
+    setoid_rewrite qq in q.
+    clear q' qq.
+    setoid_rewrite <- q.
+    setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+
+    apply ndr_comp_respects; try reflexivity.
+    Transparent nd_id.
+    simpl.
+    apply (cndr_inert pl_cnd); auto; ndpc_tac.
+    Qed.
+
+  Instance Types_cancell   : Types_second [] <~~~> functor_id _ :=
+    { ni_iso := Types_cancell_iso }.
+    apply Types_cancell_lemma.
+    Defined.
+
+  Lemma TypesL_assoc_central a b c : CentralMorphism(H:=Types_binoidal) #((Types_assoc a b) c).
+    intros.
+      apply Build_CentralMorphism.
+      intros.
+      unfold bin_obj.
+      unfold ebc_bobj.
+      Opaque nd_id.
+      simpl.
+      unfold ehom.
+      nd_swap_ltac p PL.
+      setoid_rewrite p.
+      clear p.
+      setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
+      setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
+      repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
+
+      set (ni_commutes' (jud_mon_cancelr PL) g) as q.
+      Opaque nd_id.
+      simpl in q.
+      setoid_rewrite <- q.
+      clear q.
+
+      set (ni_commutes' (jud_mon_cancell PL) g) as q.      
+      simpl in q.
+      set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
+      set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+      simpl in qq.
+      setoid_rewrite qq in q.
+      clear q' qq.
+      setoid_rewrite <- q.
+
+      setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      apply ndr_comp_respects.
+      reflexivity.
+      
+      Transparent nd_id.
+      apply (cndr_inert pl_cnd); auto; ndpc_tac.
+
+      Opaque nd_id.
+      intros.
+      unfold bin_obj.
+      unfold ebc_bobj.
+      simpl.
+      unfold ehom.
+      symmetry.
+      nd_swap_ltac p PL.
+      setoid_rewrite p.
+      clear p.
+      setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
+      setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
+      repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
+
+      set (ni_commutes' (jud_mon_cancelr PL) g) as q.
+      Opaque nd_id.
+      simpl in q.
+      setoid_rewrite <- q.
+      clear q.
+
+      set (ni_commutes' (jud_mon_cancell PL) g) as q.      
+      simpl in q.
+      set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
+      set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+      simpl in qq.
+      setoid_rewrite qq in q.
+      clear q' qq.
+      setoid_rewrite <- q.
+
+      setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      apply ndr_comp_respects.
+      reflexivity.
+      
+      Transparent nd_id.
+      apply (cndr_inert pl_cnd); auto; ndpc_tac.
+      Qed.
+
+  Lemma TypesL_cancell_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancell a).
+    intros.
+      apply Build_CentralMorphism.
+      Opaque nd_id.
+      intros.
+      unfold bin_obj.
+      unfold ebc_bobj.
+      simpl.
+      unfold ehom.
+      nd_swap_ltac p PL.
+      setoid_rewrite p.
+      clear p.
+      setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
+      setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
+      repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
+
+      set (ni_commutes' (jud_mon_cancelr PL) g) as q.
+      Opaque nd_id.
+      simpl in q.
+      setoid_rewrite <- q.
+      clear q.
+
+      set (ni_commutes' (jud_mon_cancell PL) g) as q.      
+      simpl in q.
+      set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
+      set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+      simpl in qq.
+      setoid_rewrite qq in q.
+      clear q' qq.
+      setoid_rewrite <- q.
+
+      setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      apply ndr_comp_respects.
+      reflexivity.
+      
+      Transparent nd_id.
+      apply (cndr_inert pl_cnd); auto; ndpc_tac.
+
+      Opaque nd_id.
+      intros.
+      unfold bin_obj.
+      unfold ebc_bobj.
+      simpl.
+      unfold ehom.
+      symmetry.
+      nd_swap_ltac p PL.
+      setoid_rewrite p.
+      clear p.
+      setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
+      setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
+      repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
+
+      set (ni_commutes' (jud_mon_cancelr PL) g) as q.
+      Opaque nd_id.
+      simpl in q.
+      setoid_rewrite <- q.
+      clear q.
+
+      set (ni_commutes' (jud_mon_cancell PL) g) as q.      
+      simpl in q.
+      set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
+      set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+      simpl in qq.
+      setoid_rewrite qq in q.
+      clear q' qq.
+      setoid_rewrite <- q.
+
+      setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      apply ndr_comp_respects.
+      reflexivity.
+      
+      Transparent nd_id.
+      apply (cndr_inert pl_cnd); auto; ndpc_tac.
+      Qed.
+
+  Lemma TypesL_cancelr_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancelr a).
+    intros.
+      apply Build_CentralMorphism.
+      Opaque nd_id.
+      intros.
+      unfold bin_obj.
+      unfold ebc_bobj.
+      simpl.
+      unfold ehom.
+      nd_swap_ltac p PL.
+      setoid_rewrite p.
+      clear p.
+      setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
+      setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
+      repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
+
+      set (ni_commutes' (jud_mon_cancelr PL) g) as q.
+      Opaque nd_id.
+      simpl in q.
+      setoid_rewrite <- q.
+      clear q.
+
+      set (ni_commutes' (jud_mon_cancell PL) g) as q.      
+      simpl in q.
+      set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
+      set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+      simpl in qq.
+      setoid_rewrite qq in q.
+      clear q' qq.
+      setoid_rewrite <- q.
+
+      setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      apply ndr_comp_respects.
+      reflexivity.
+      
+      Transparent nd_id.
+      apply (cndr_inert pl_cnd); auto; ndpc_tac.
+
+      Opaque nd_id.
+      intros.
+      unfold bin_obj.
+      unfold ebc_bobj.
+      simpl.
+      unfold ehom.
+      symmetry.
+      nd_swap_ltac p PL.
+      setoid_rewrite p.
+      clear p.
+      setoid_rewrite (@nd_prod_split_left  _ Rule PL _ _ _ []).
+      setoid_rewrite (@nd_prod_split_right _ Rule PL _ _ _ []).
+      repeat setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      setoid_rewrite <- (@ndr_comp_associativity _ Rule PL).
+
+      set (ni_commutes' (jud_mon_cancelr PL) g) as q.
+      Opaque nd_id.
+      simpl in q.
+      setoid_rewrite <- q.
+      clear q.
+
+      set (ni_commutes' (jud_mon_cancell PL) g) as q.      
+      simpl in q.
+      set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal PL)))) as q'.
+      set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+      simpl in qq.
+      setoid_rewrite qq in q.
+      clear q' qq.
+      setoid_rewrite <- q.
+
+      setoid_rewrite (@ndr_comp_associativity _ Rule PL).
+      apply ndr_comp_respects.
+      reflexivity.
+      
+      Transparent nd_id.
+      apply (cndr_inert pl_cnd); auto; ndpc_tac.
+      Qed.
+
+  Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
+    { pmon_assoc    := Types_assoc
+    ; pmon_cancell  := Types_cancell
+    ; pmon_cancelr  := Types_cancelr
+    ; pmon_assoc_rr := Types_assoc_rr
+    ; pmon_assoc_ll := Types_assoc_ll
+    }.
+    abstract (apply Build_Pentagon; intros; simpl; eapply cndr_inert; try apply PL; ndpc_tac).
+    abstract (apply Build_Triangle; intros; simpl; eapply cndr_inert; try apply PL; ndpc_tac).
+    intros; simpl; reflexivity.
+    intros; simpl; reflexivity.
+    apply TypesL_assoc_central.
+    apply TypesL_cancelr_central.
+    apply TypesL_cancell_central.
+    Defined.
+
+End ProgrammingLanguageCategory.
+

diff --git a/src/ProgrammingLanguageEnrichment.v b/src/ProgrammingLanguageEnrichment.v
new file mode 100644 (file)
index 0000000..332a8ba
--- /dev/null
+++ b/src/ProgrammingLanguageEnrichment.v
@@ -0,0 +1,52 @@
+(*********************************************************************************************************************************)
+(* ProgrammingLanguageEnrichment                                                                                                 *)
+(*                                                                                                                               *)
+(*   Types are enriched in Judgments.                                                                                            *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Categories_ch1_3.
+Require Import InitialTerminal_ch2_2.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import OppositeCategories_ch1_6_2.
+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 MonoidalCategories_ch7_8.
+Require Import Coherence_ch7_8.
+Require Import Enrichment_ch2_8.
+Require Import RepresentableStructure_ch7_2.
+Require Import FunctorCategories_ch7_7.
+
+Require Import Enrichments.
+Require Import NaturalDeduction.
+Require Import NaturalDeductionCategory.
+Require Import ProgrammingLanguageCategory.
+        Export ProgrammingLanguageCategory.
+
+Section ProgrammingLanguageEnrichment.
+
+  Context `(PL:ProgrammingLanguage).
+
+  Definition TypesEnrichedInJudgments : SurjectiveEnrichment.
+    refine
+      {| senr_c_pm     := TypesL_PreMonoidal PL
+       ; senr_v        := JudgmentsL PL
+       ; senr_v_bin    := Judgments_Category_binoidal _
+       ; senr_v_pmon   := Judgments_Category_premonoidal _
+       ; senr_v_mon    := Judgments_Category_monoidal _
+       ; senr_c_bin    := Types_binoidal PL
+       ; senr_c        := TypesL PL
+      |}.
+      Defined.
+
+End ProgrammingLanguageEnrichment.
+

diff --git a/src/ProgrammingLanguageFlattening.v b/src/ProgrammingLanguageFlattening.v
index 4438dd2..4c2a66b 100644 (file)
--- a/src/ProgrammingLanguageFlattening.v
+++ b/src/ProgrammingLanguageFlattening.v
@@ -27,7 +27,7 @@ Require Import Reification.
 Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 Require Import GeneralizedArrow.
-Require Import ProgrammingLanguage.
+Require Import ProgrammingLanguageEnrichment.
 Require Import ProgrammingLanguageReification.
 Require Import SectionRetract_ch2_4.
 Require Import GeneralizedArrowFromReification.

diff --git a/src/ProgrammingLanguageGeneralizedArrow.v b/src/ProgrammingLanguageGeneralizedArrow.v
index bed54b6..8fe0391 100644 (file)
--- a/src/ProgrammingLanguageGeneralizedArrow.v
+++ b/src/ProgrammingLanguageGeneralizedArrow.v
@@ -30,7 +30,7 @@ Require Import NaturalDeductionCategory.
 Require Import Enrichments.
 Require Import Reification.
 Require Import GeneralizedArrow.
-Require Import ProgrammingLanguage.
+Require Import ProgrammingLanguageEnrichment.
 
 Section ProgrammingLanguageGeneralizedArrow.
 

diff --git a/src/ProgrammingLanguageReification.v b/src/ProgrammingLanguageReification.v
index 932c517..c1a06d8 100644 (file)
--- a/src/ProgrammingLanguageReification.v
+++ b/src/ProgrammingLanguageReification.v
@@ -28,6 +28,7 @@ Require Import Reification.
 Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 Require Import ProgrammingLanguage.
+Require Import ProgrammingLanguageCategory.
 Require Import Enrichments.
 
 Section ProgrammingLanguageReification.