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

• https://mathoverflow.net/a/136480

def CategoryTheory.uniqueHomsetOfInitialIsoUnit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] [CategoryTheory.CartesianClosed C] [CategoryTheory.Limits.HasInitial C] (i : ⊥_ C ≅ 𝟙_ C) (X Y : C) : Unique (X ⟶ Y)

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.

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

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.

def CategoryTheory.equivPUnit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] [CategoryTheory.CartesianClosed C] [CategoryTheory.Limits.HasZeroObject C] : C ≌ CategoryTheory.Discrete PUnit.{w + 1}

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.