normalize

Mathlib.CategoryTheory.Bicategory.Coherence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.FreeBicategory.normalize

Lean4

/-- The normalization pseudofunctor for the free bicategory on a quiver `B`. -/
def normalize (B : Type u) [Quiver.{v + 1} B] : Pseudofunctor (FreeBicategory B) (LocallyDiscrete (Paths B))
    where
  obj a := ⟨a⟩
  map f := ⟨normalizeAux nil f⟩
  map₂ η := eqToHom <| Discrete.ext <| normalizeAux_congr nil η
  mapId _ := eqToIso <| Discrete.ext rfl
  mapComp f g := eqToIso <| Discrete.ext <| normalizeAux_nil_comp f g

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

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

Разделы

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

Аффилиация

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