naturality_whiskerRight

Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

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

Lean4

theorem naturality_whiskerRight {p f g h pf pfh : C} {η : f ≅ g} (η_f : p ⊗ f ≅ pf) (η_g : p ⊗ g ≅ pf)
    (η_fh : (pf ⊗ h) ≅ pfh) (ih_η : p ◁ η ≪≫ η_g = η_f) :
    p ◁ (η ▷ h) ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp η_f η_fh :=
  by
  rw [← ih_η]
  apply Iso.ext
  simp

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

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

Разделы

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

Аффилиация

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