inclusionPathAux

Mathlib.CategoryTheory.Bicategory.Coherence

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

Lean4

/-- Auxiliary definition for `inclusionPath`. -/
@[simp]
def inclusionPathAux {a : B} : ∀ {b : B}, Path a b → Hom a b
  | _, nil => Hom.id a
  | _, cons p f => (inclusionPathAux p).comp (Hom.of f)

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

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

Разделы

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

Аффилиация

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