hComp

Mathlib.CategoryTheory.Bicategory.CatEnriched

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CatEnrichedOrdinary.hComp

Lean4

/-- The horizontal composition on 2-morphisms is defined using the action on arrows of the
composition bifunctor from the enriched category structure. -/
def hComp {a b c : CatEnrichedOrdinary C} {f f' : a ⟶ b} {g g' : b ⟶ c} (η : f ⟶ f') (θ : g ⟶ g') : f ≫ g ⟶ f' ≫ g' :=
  .mk <| eqToHom (homEquiv_comp f g) ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom (homEquiv_comp f' g').symm

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

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

Разделы

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

Аффилиация

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