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

@[implicit_reducible]

noncomputable def CategoryTheory.uniqueHomsetOfInitialIsoUnit {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [MonoidalClosed C] [Limits.HasInitial C] (i : ⊥_ C ≅ MonoidalCategoryStruct.tensorUnit 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.

@[implicit_reducible]

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

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

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

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