assoc'

Mathlib.Tactic.CategoryTheory.MonoidalComp

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCoherence.assoc'

Lean4

@[simps]
instance assoc' (W X Y Z : C) [MonoidalCoherence W (X ⊗ (Y ⊗ Z))] : MonoidalCoherence W ((X ⊗ Y) ⊗ Z) :=
  ⟨ ⊗𝟙 ≪≫ (α_ X Y Z).symm⟩

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

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

Разделы

Аффилиация

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