whiskerRight

Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Oplax.OplaxTrans.whiskerRight

Lean4

/-- Right whiskering of an oplax natural transformation and a modification. -/
@[simps]
def whiskerRight {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) : η ≫ ι ⟶ θ ≫ ι
    where
  app a := Γ.app a ▷ ι.app a
  naturality {a b}
    f := by
    dsimp
    simp_rw [assoc, ← associator_inv_naturality_left, whisker_exchange_assoc]
    simp

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

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

Разделы

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

Аффилиация

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