; freyd_C_cartesian : CartesianCat freyd_C_monoidal
; freyd_K_binoidal :> BinoidalCat freyd_K freyd_bobj
; freyd_K_monoidal :> PreMonoidalCat freyd_K_binoidal (one(Terminal:=freyd_C_terminal))
; freyd_C_cartesian : CartesianCat freyd_C_monoidal
; freyd_K_binoidal :> BinoidalCat freyd_K freyd_bobj
; freyd_K_monoidal :> PreMonoidalCat freyd_K_binoidal (one(Terminal:=freyd_C_terminal))