Theorems · Theorem · category theory

CategoryTheory.Monad.monadMonEquiv_counitIso_hom_app_hom

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.Mon (CategoryTheory.Functor C C)),
  ((CategoryTheory.Monad.monadMonEquiv C).counitIso.hom.app x).hom =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Monad.monToMonad C).comp (CategoryTheory.Monad.monadToMon C)).obj x).X

Defined in

Mathlib.CategoryTheory.Monad.EquivMon

Cited by

0 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category