cartesian package:monoidal-functors

A Category equipped with a Tensor t where the Tensor unit i is the terminal object in cat and thus every object a is equipped with a morphism <math>, which we call kill.

Laws

fwd unitl . glmap kill . splitid
fwd unitr . grmap kill . splitid
A Category equipped with a Tensor t where the Tensor unit i is the initial object in cat and thus every object a is equipped with a morphism <math>, which we call spawn.

Laws

merge . glmap spawn . bwd unitlid
merge . grmap spawn . bwd unitrid
A Category is Semicartesian if it is equipped with a Symmetric bifunctor t and each object comes equipped with a diagonal morphism <math>, which we call split.

Laws

grmap split . splitbwd assoc . glmap split . split
glmap split . splitfwd assoc . grmap split . split
A Category is Semicocartesian if it is equipped with a Symmetric type operator t and each object comes equipped with a morphism <math>, which we call merge.

Laws

merge . grmap mergemerge . glmap merge . fwd assoc
merge . glmap mergemerge . grmap merge . bwd assoc