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.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) : 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.Limits.HasFiniteProducts C] [CategoryTheory.CartesianClosed C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (Y : C) : Unique (X ⟶ Y)

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

Equations

• CategoryTheory.uniqueHomsetOfZero X Y = CategoryTheory.uniqueHomsetOfInitialIsoTerminal (CategoryTheory.Iso.mk default (CategoryTheory.CategoryStruct.comp default default)) X Y

def CategoryTheory.equivPUnit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts 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.