equiv

Mathlib.CategoryTheory.Category.ULift

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ULiftHomULiftCategory.equiv

Lean4

/-- The equivalence between `C` and `ULiftHom (ULift C)`. -/
def equiv.{v', u', v, u} (C : Type u) [Category.{v} C] : C ≌ ULiftHom.{v'} (ULift.{u'} C) :=
  ULift.equivalence.trans ULiftHom.equiv

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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