# 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 #

def
CategoryTheory.uniqueHomsetOfInitialIsoTerminal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.CartesianClosed C]
[CategoryTheory.Limits.HasInitial C]
(i : ⊥_ C ≅ ⊤_ C)
(X : C)
(Y : C)
:

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

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

def
CategoryTheory.uniqueHomsetOfZero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.CartesianClosed C]
[CategoryTheory.Limits.HasZeroObject C]
(X : C)
(Y : C)
:

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

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

def
CategoryTheory.equivPUnit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.CartesianClosed C]
[CategoryTheory.Limits.HasZeroObject C]
:

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

## Equations

- One or more equations did not get rendered due to their size.