X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FProgrammingLanguage.v;h=dc2256c6d7ebb403520f595036e9914f456cc63c;hp=933785af591887f446bc8a85fd9d556ae7ca4045;hb=bef99d21b3f5697d6fb1871493290c8dcf9dea93;hpb=64d416692bda1d36c33b5efa245d46dcf546ad4a diff --git a/src/ProgrammingLanguage.v b/src/ProgrammingLanguage.v index 933785a..dc2256c 100644 --- 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. @@ -116,7 +116,7 @@ Section Programming_Language. simpl; eapply cndr_inert. apply pl_eqv. auto. auto. Defined. - Definition Types_binoidal : EBinoidalCat TypesL. + Definition Types_binoidal : EBinoidalCat TypesL (@T_Branch _). refine {| ebc_first := Types_first ; ebc_second := Types_second @@ -169,41 +169,507 @@ Section Programming_Language. 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; unfold eqv; simpl. - admit. - Defined. + 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; simpl. - admit. + 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 }. - admit. - 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 }. - admit. - 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) }. - admit. + 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_PreMonoidal : PreMonoidalCat Types_binoidal [] := + 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. @@ -229,6 +695,7 @@ Section Programming_Language. auto. auto. auto. + apply Build_Triangle; intros; simpl. eapply cndr_inert. apply pl_eqv. auto. @@ -241,54 +708,26 @@ Section Programming_Language. auto. eapply cndr_inert. apply pl_eqv. auto. auto. -*) -admit. -admit. intros; simpl; reflexivity. intros; simpl; reflexivity. - admit. (* assoc central *) - admit. (* cancelr central *) - admit. (* cancell central *) + apply TypesL_assoc_central. + apply TypesL_cancelr_central. + apply TypesL_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 ].