Theorems · Definition · algebraic topology

SSet.Truncated.HomotopyCategory.isTerminal

(X : SSet.Truncated 2) →
  [Unique (X.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 }))] →
    [Subsingleton (X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.ι0₂._proof_5 }))] →
      CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of X.HomotopyCategory)

If X : Truncated 2 has a unique 0-simplex and (at most) one 1-simplex, then X.HomotopyCategory is a terminal object in Cat.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniqueSubsingleton