hComp

Mathlib.CategoryTheory.Functor.TwoSquare

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

Lean4

/-- The horizontal composition of 2-squares. -/
@[simps!]
def hComp (w : TwoSquare T L R B) (w' : TwoSquare T' R R' B') : TwoSquare (T ⋙ T') L R' (B ⋙ B') :=
  .mk _ _ _ _ <|
    (associator _ _ _).hom ≫
      (whiskerLeft T w'.natTrans) ≫ (associator _ _ _).inv ≫ (whiskerRight w.natTrans B') ≫ (associator _ _ _).hom

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

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

Разделы

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

Аффилиация

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