instUniqueOneTruncation₂DeltaZero

English

Since ⦋0⦌ is terminal in SimplexCategory, Δ[0] has a unique point and hence OneTruncation₂ of truncation 2 of Δ[0] has a unique inhabitant.

Русский

Поскольку ⦋0⦌ является терминальным в SimplexCategory, Δ[0] имеет единственную точку, и значит OneTruncation₂((truncation 2).obj Δ[0]) имеет единственный элемент.

LaTeX

$$Unique (OneTruncation₂ ((truncation 2).obj Δ[0]))$$

Lean4

/-- Since `⦋0⦌ : SimplexCategory` is terminal, `Δ[0]` has a unique point and thus
`OneTruncation₂ ((truncation 2).obj Δ[0])` has a unique inhabitant. -/
instance instUniqueOneTruncation₂DeltaZero : Unique (OneTruncation₂ ((truncation 2).obj Δ[0])) :=
  inferInstanceAs (Unique (ULift.{_, 0} (⦋0⦌ ⟶ ⦋0⦌)))

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