English
The object hoFunctor.obj (Δ[0]) is a terminal object in the homotopy category.
Русский
Объект hoFunctor.obj(Δ[0]) является терминальным объектом в гомотопической категории.
LaTeX
$$$IsTerminal\\big( hoFunctor.obj (\\Delta[0]) \\big)$$$
Lean4
/-- The category `hoFunctor.obj (Δ[0])` is terminal. -/
def isTerminalHoFunctorDeltaZero : IsTerminal (hoFunctor.obj (Δ[0])) :=
by
letI : Unique ((truncation 2).obj Δ[0]).HomotopyCategory :=
inferInstanceAs (Unique <| CategoryTheory.Quotient Truncated.HoRel₂)
letI sub : Subsingleton ((truncation 2).obj Δ[0]).HomotopyCategory := by infer_instance
letI : IsDiscrete ((truncation 2).obj Δ[0]).HomotopyCategory :=
{ subsingleton X Y := inferInstanceAs <| Subsingleton ((_ : CategoryTheory.Quotient Truncated.HoRel₂) ⟶ _)
eq_of_hom f := sub.allEq _ _ }
apply Cat.isTerminalOfUniqueOfIsDiscrete
