Theorems · Definition · algebraic topology

SSet.Truncated.HomotopyCategory.isoTerminal

(X : SSet.Truncated 2) →
  [Unique (X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))] →
    [Subsingleton
          (X.obj
            (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.HomotopyCategory.isoTerminal._proof_1 }))] →
      CategoryTheory.Cat.of X.HomotopyCategory ≅ CategoryTheory.Cat.chosenTerminal

If X : Truncated 2 has a unique 0-simplex and (at most) one 1-simplex, this is the isomorphism Cat.of X.HomotopyCategory ≅ Cat.chosenTerminal in Cat.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniqueSubsingleton