- (* need to prove that if we have cartesian tuples we have cartesian contexts *)
- Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
- admit.
+ 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.
+*)
+admit.
+admit.
+ intros; simpl; reflexivity.
+ intros; simpl; reflexivity.
+ admit. (* assoc central *)
+ admit. (* cancelr central *)
+ admit. (* 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
+ |}.