+ Definition Types_cancelr : Types_first [] <~~~> functor_id _.
+ admit.
+ Defined.
+
+ Definition Types_cancell : Types_second [] <~~~> functor_id _.
+ admit.
+ Defined.
+
+ Definition Types_assoc_ll a b : Types_second (a,,b) <~~~> Types_second b >>>> Types_second a.
+ admit.
+ Defined.
+
+ Definition Types_assoc_rr a b : Types_first (a,,b) <~~~> Types_first a >>>> Types_first b.
+ admit.
+ Defined.
+
+ Instance Types_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
+ }.
+ admit. (* pentagon law *)
+ admit. (* triangle law *)
+ admit. (* assoc_rr/assoc coherence *)
+ admit. (* assoc_ll/assoc coherence *)
+ Defined.
+