asTypeEquivObjAsType — Mathlib

English

There is an equivalence between AsType α and ObjAsType α given by the two canonical functors.

Русский

Существует эквивалентность между AsType α и ObjAsType α, заданная двумя каноническими функторaми.

LaTeX

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

Lean4

/-- The constructed category (`AsType α`) is equivalent to `ObjAsType α`. -/
noncomputable def asTypeEquivObjAsType : AsType α ≌ ObjAsType α
    where
  functor := asTypeToObjAsType α
  inverse := objAsTypeToAsType α
  unitIso := NatIso.ofComponents Iso.refl
  counitIso := NatIso.ofComponents Iso.refl

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