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
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 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.
+ admit. (* need to add this as an obligation in ProgrammingLanguage class *)
Defined.
Instance Types_cancelr : Types_first [] <~~~> functor_id _ :=
{ ni_iso := Types_cancelr_iso }.
intros; simpl.
- admit.
+ admit. (* need to add this as an obligation in ProgrammingLanguage class *)
Defined.
Instance Types_cancell : Types_second [] <~~~> functor_id _ :=
{ ni_iso := Types_cancell_iso }.
- admit.
+ admit. (* need to add this as an obligation in ProgrammingLanguage class *)
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.
+ admit. (* need to add this as an obligation in ProgrammingLanguage class *)
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.
+ admit. (* need to add this as an obligation in ProgrammingLanguage class *)
Defined.
Instance TypesL_PreMonoidal : PreMonoidalCat Types_binoidal [] :=
; pmon_assoc_rr := Types_assoc_rr
; pmon_assoc_ll := Types_assoc_ll
}.
-(*
apply Build_Pentagon.
intros; simpl.
eapply cndr_inert. apply pl_eqv.
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 *)
+ admit. (* assoc is central: need to add this as an obligation in ProgrammingLanguage class *)
+ admit. (* cancelr is central: need to add this as an obligation in ProgrammingLanguage class *)
+ admit. (* cancell is central: need to add this as an obligation in ProgrammingLanguage class *)
Defined.
Definition TypesEnrichedInJudgments : SurjectiveEnrichment.