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