mkOfHomPrefunctors

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors

Lean4

/-- Construct a lax prefunctor from a map on objects, and prefunctors between the corresponding
hom types. -/
@[simps]
def mkOfHomPrefunctors (F : B → C) (F' : (a : B) → (b : B) → Prefunctor (a ⟶ b) (F a ⟶ F b)) : PrelaxFunctorStruct B C
    where
  obj := F
  map {a b} := (F' a b).obj
  map₂ {a b} := (F' a b).map

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

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

Разделы

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

Аффилиация

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