typeToCat

Mathlib.CategoryTheory.Category.Cat

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

Lean4

/-- Embedding `Type` into `Cat` as discrete categories.

This ought to be modelled as a 2-functor!
-/
@[simps]
def typeToCat : Type u ⥤ Cat where
  obj X := Cat.of (Discrete X)
  map := fun f => Discrete.functor (Discrete.mk ∘ f)
  map_id
    X := by
    apply Functor.ext
    · intro X Y f
      cases f
      simp only [eqToHom_refl, Cat.id_map, Category.comp_id, Category.id_comp]
      apply ULift.ext
      cat_disch
    · simp
  map_comp f g := by apply Functor.ext; cat_disch

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

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

Разделы

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

Аффилиация

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