terminalIso — Mathlib

English

There is a unique morphism between any two objects in the one-truncation of Δ[0] at truncation 2.

Русский

Между любыми двумя объектами в OneTruncation₂((truncation 2).obj Δ[0]) существует единственный морфизм.

LaTeX

$$Unique ((x ⟶ y) for x,y in OneTruncation₂((truncation 2).obj Δ[0]))$$

Lean4

/-- The homotopy category functor preserves generic terminal objects. -/
noncomputable def terminalIso : hoFunctor.obj (⊤_ SSet) ≅ ⊤_ Cat :=
  hoFunctor.mapIso (terminalIsoIsTerminal stdSimplex.isTerminalObj₀) ≪≫
    (terminalIsoIsTerminal isTerminalHoFunctorDeltaZero).symm

Похожие утверждения