objAsTypeEquiv — Mathlib

English

Let α be a category equipped with a countable structure. Then the category ObjAsType(α) is equivalent to α.

Русский

Пусть α — категория с счетной структурой. Тогда объекты ObjAsType(α) эквивалентны α.

LaTeX

$$$\mathrm{ObjAsType}(\alpha) \simeq \alpha$$$

Lean4

/-- The constructed category is indeed equivalent to `α`. -/
noncomputable def objAsTypeEquiv : ObjAsType α ≌ α :=
  (inducedFunctor (equivShrink.{0} α).symm).asEquivalence

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