instIsMonoidalMonoidalOppositeMopMopEquivalence

English

The equivalence mopMopEquivalence is monoidal.

Русский

Эквивалентность MopMopEquivalence моноидальная.

LaTeX

$$$$ \\operatorname{IsMonoidal}\\bigl( \\mathrm{mopMopEquivalence}(C) \\bigr) $$$$

Lean4

instance : (mopMopEquivalence C).IsMonoidal
    where
  leftAdjoint_ε := by simp [ε, η, Adjunction.homEquiv, mopMopEquivalence, Equivalence.trans, unmopEquiv, ε]
  leftAdjoint_μ X Y := by simp [μ, δ, Adjunction.homEquiv, mopMopEquivalence, Equivalence.trans, unmopEquiv, μ]

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