terminalEquiv — Mathlib

English

There is an equivalence between IsTerminal X and Unique (ToType X).

Русский

Существует эквивалентность между IsTerminal X и Unique(ToType X).

LaTeX

$$$ \\text{terminalEquiv } X : IsTerminal X \\simeq Unique (ToType X) $$$

Lean4

/-- The equivalence `ToType (⊤_ C) ≃ PUnit` when `C` is a concrete category. -/
noncomputable def terminalEquiv : ToType (⊤_ C) ≃ PUnit :=
  (PreservesTerminal.iso (forget C) ≪≫ Types.terminalIso).toEquiv

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