ofTypeFunctor

Mathlib.CategoryTheory.Types.Basic

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

Lean4

/-- `ofTypeFunctor m` converts from Lean's `Type`-based `Category` to `CategoryTheory`. This
allows us to use these functors in category theory. -/
def ofTypeFunctor (m : Type u → Type v) [_root_.Functor m] [LawfulFunctor m] : Type u ⥤ Type v
    where
  obj := m
  map f := _root_.Functor.map f
  map_id := fun α => by funext X; apply id_map

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

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

Разделы

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

Аффилиация

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