def SimplexCategory.isTerminalZero : CategoryTheory.Limits.IsTerminal (SimplexCategory.mk 0)

The object [0] is terminal in SimplexCategory.

Equations

• SimplexCategory.isTerminalZero = CategoryTheory.Limits.IsTerminal.ofUniqueHom (fun (x : SimplexCategory) => x.const (SimplexCategory.mk 0) 0) ⋯