mathlib3 documentation

category_theory.closed.zero

A cartesian closed category with zero object is trivial #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

References #