Theorems · Theorem · category theory

CategoryTheory.equiv_punit_iff_unique

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  Nonempty (C ≌ CategoryTheory.Discrete PUnit.{w + 1}) ↔ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))

A category being equivalent to PUnit is equivalent to it having a unique morphism between any two objects. (In fact, such a category is also a groupoid; see CategoryTheory.Groupoid.ofHomUnique)

Defined in

Mathlib.CategoryTheory.PUnit

Cited by

0 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category