instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison

English

If R is monadic, then the Monad comparison of the monadic adjunction is an equivalence.

Русский

Если R является монадическим, то сопоставление монад сопряжения монадического является эквивалентностью.

LaTeX

$$$$\\text{IsEquivalence}(\\mathrm{Monad.comparison}(\\mathrm{monadicAdjunction } R))$$$$

Lean4

instance (R : D ⥤ C) [MonadicRightAdjoint R] : (Monad.comparison (monadicAdjunction R)).IsEquivalence :=
  MonadicRightAdjoint.eqv

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