naturality_rightUnitor

Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

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

Lean4

theorem naturality_rightUnitor {p f pf : C} (η_f : p ⊗ f ≅ pf) : p ◁ (ρ_ f) ≪≫ η_f = normalizeIsoComp η_f (ρ_ pf) :=
  Iso.ext (by simp)

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

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

Разделы

Аффилиация

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