instIsCorepresentableIdType

Mathlib.CategoryTheory.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instIsCorepresentableIdType

English

The identity functor on Type v is corepresentable.

Русский

Функтор тождественный на Type является корпредставляющим.

LaTeX

$$$ \\text{Functor.Id}_{\\mathbf{Type}} \\text{ is corepresentable} $$$

Lean4

instance : Functor.IsCorepresentable (𝟭 (Type v₁)) :=
  corepresentable_of_natIso (coyoneda.obj (op PUnit)) Coyoneda.punitIso

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru