naturality_associator

Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Monoidal.naturality_associator

Lean4

theorem naturality_associator {p f g h pf pfg pfgh : C} (η_f : p ⊗ f ≅ pf) (η_g : pf ⊗ g ≅ pfg) (η_h : pfg ⊗ h ≅ pfgh) :
    p ◁ (α_ f g h) ≪≫ normalizeIsoComp η_f (normalizeIsoComp η_g η_h) =
      normalizeIsoComp (normalizeIsoComp η_f η_g) η_h :=
  Iso.ext (by simp)

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

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

Разделы

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

Аффилиация

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