English
Between any two objects x,y in OneTruncation₂((truncation 2).obj Δ[0]), there is a unique morphism.
Русский
Между любыми двумя объектами x,y в OneTruncation₂((truncation 2).obj Δ[0]) существует единственный морфизм.
LaTeX
$$Unique (x ⟶ y) for all x,y ∈ OneTruncation₂((truncation 2).obj Δ[0])$$
Lean4
/-- Since `⦋0⦌ : SimplexCategory` is terminal, `Δ[0]` has a unique edge and thus the homs of
`OneTruncation₂ ((truncation 2).obj Δ[0])` have unique inhabitants. -/
instance (x y : OneTruncation₂ ((truncation 2).obj Δ[0])) : Unique (x ⟶ y)
where
default := by
obtain rfl : x = default := Unique.uniq _ _
obtain rfl : y = default := Unique.uniq _ _
exact 𝟙rq instUniqueOneTruncation₂DeltaZero.default
uniq
_ :=
by
letI : Subsingleton (((truncation 2).obj Δ[0]).obj (.op ⦋1⦌₂)) :=
inferInstanceAs (Subsingleton (ULift.{_, 0} (⦋1⦌ ⟶ ⦋0⦌)))
ext
exact this.allEq _ _
