uliftCategory

Mathlib.CategoryTheory.Category.Basic

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

Lean4

/-- The category structure on `ULift C` that is induced from the category
structure on `C`. This is not made a global instance because of a diamond
when `C` is a preordered type. -/
def uliftCategory : Category.{v} (ULift.{u'} C)
    where
  Hom X Y := X.down ⟶ Y.down
  id X := 𝟙 X.down
  comp f g := f ≫ g

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

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

Разделы

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

Аффилиация

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