mopMopEquivalenceInverseMonoidal

Mathlib.CategoryTheory.Monoidal.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalOpposite.mopMopEquivalenceInverseMonoidal

Lean4

@[simps!]
instance mopMopEquivalenceInverseMonoidal : (MonoidalOpposite.mopMopEquivalence C).inverse.Monoidal
    where
  ε := 𝟙 _
  δ X Y := 𝟙 _
  μ X Y := 𝟙 _
  η := 𝟙 _
  ε_η := Category.comp_id _
  η_ε := Category.comp_id _
  μ_δ X Y := Category.comp_id _
  δ_μ X Y := Category.comp_id _

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

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

Разделы

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

Аффилиация

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