tensor_right

Mathlib.Tactic.CategoryTheory.MonoidalComp

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

Lean4

@[simps]
instance tensor_right (X Y : C) [MonoidalCoherence (𝟙_ C) Y] : MonoidalCoherence X (X ⊗ Y) :=
  ⟨(ρ_ X).symm ≪≫ (whiskerLeftIso X ⊗𝟙 )⟩

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

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

Разделы

Аффилиация

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