English
An object Y is terminal if and only if for every X there exists a unique morphism X → Y; this is equivalent to an equivalence between IsLimit on the cone with apex Y and the family of Unique morphisms to Y.
Русский
Объект Y является терминальным тогда и только тогда, когда для каждого X существует единственный морфизм X → Y; это эквивалентно существованию эквивалентности между IsLimit для конуса с вершиной Y и семейством уникальных морфизмов к Y.
LaTeX
$$$\text{IsTerminalEquivUnique}(F,Y) : \text{IsLimit}(\langle Y,\dots\rangle) \simeq \forall X\,\Unique(X \to Y).$$$
Lean4
/-- To show a category is an `InitialMonoClass` it suffices to show the unique morphism from an
initial object to a terminal object is a monomorphism. -/
theorem of_isTerminal {I T : C} (hI : IsInitial I) (hT : IsTerminal T) (_ : Mono (hI.to T)) : InitialMonoClass C :=
InitialMonoClass.of_isInitial hI fun X => mono_of_mono_fac (hI.hom_ext (_ ≫ hT.from X) (hI.to T))
