mathlib documentation

category_theory.closed.zero

A cartesian closed category with zero object is trivial #

A cartesian closed category with zero object is trivial: it is equivalent to the category with one object and one morphism.

References #