`(C:CartesianCat(Ob:=Ob)(C:=C1)(bin_obj':=bobj))
(* a premonoidal category K with the same objects (its unit object is 1 because the functor is both IIO and strict) *)
`(C:CartesianCat(Ob:=Ob)(C:=C1)(bin_obj':=bobj))
(* a premonoidal category K with the same objects (its unit object is 1 because the functor is both IIO and strict) *)