typeToCatObjectsAdj

Mathlib.CategoryTheory.Category.Cat.Adjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Cat.typeToCatObjectsAdj

Lean4

/-- `typeToCat : Type ⥤ Cat` is left adjoint to `Cat.objects : Cat ⥤ Type` -/
def typeToCatObjectsAdj : typeToCat ⊣ Cat.objects :=
  Adjunction.mk'
    { homEquiv := typeToCatObjectsAdjHomEquiv
      unit := { app := fun _ ↦ Discrete.mk }
      counit :=
        { app := typeToCatObjectsAdjCounitApp
          naturality := fun _ _ _ ↦
            Functor.hext (fun _ ↦ rfl)
              (by
                intro ⟨_⟩ ⟨_⟩ f
                obtain rfl := Discrete.eq_of_hom f
                cat_disch) } }

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

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

Разделы

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

Аффилиация

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