instHasTerminalTopOfContainsIdentities

English

If P is a morphism property containing identities, then the Over category P.Over ⊤ X has a terminal object. This is a structural property ensuring the existence of a terminal object in a slice-like category built from P over a top morphism.

Русский

Если свойство морфизмов P содержит идентичности, то категория Over, построенная как P.Over ⊤ X, имеет терминальный объект.

LaTeX

$$$ \text{HasTerminal}(P.Over\;\top X). $$$

Lean4

instance [P.ContainsIdentities] : HasTerminal (P.Over ⊤ X) :=
  let h : IsTerminal (Over.mk ⊤ (𝟙 X) (P.id_mem X)) := Over.mkIdTerminal P X
  h.hasTerminal

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