leftUnitor_isEquivalence — Mathlib

English

The left unitor functor is an equivalence of categories with its inverse being the left inverse unitor.

Русский

Левый унитор-функтор образует эквивалентность категорий, обратной связью служит левый обратный унитор.

LaTeX

$$$(\\text{leftUnitor }\\mathcal{C}).\\text{IsEquivalence} = \\text{Equivalence of } \\mathrm{Discrete}(PUnit) \\times \\mathcal{C} \\simeq \\mathcal{C}$$$

Lean4

instance leftUnitor_isEquivalence : (leftUnitor C).IsEquivalence :=
  (leftUnitorEquivalence C).isEquivalence_functor

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