Documentation

Mathlib.CategoryTheory.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 #

If a cartesian closed category has an initial object which is isomorphic to the terminal object, then each homset has exactly one element.

Instances For

    If a cartesian closed category has a zero object, each homset has exactly one element.

    Instances For

      A cartesian closed category with a zero object is equivalent to the category with one object and one morphism.

      Instances For