case w.w.h
C : Type u₁
inst✝ : Category C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), (Monad.η M).app X ≫ f.hom.app X = (Monad.η N).app X
f_μ : ∀ (X : C), (Monad.μ M).app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ (Monad.μ N).app X
x✝ : C
⊢ ((monadToFunctor C).mapIso (MonadIso.mk f)).hom.app x✝ = f.hom.app x✝
C : Type u₁
inst✝ : Category C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), (Monad.η M).app X ≫ f.hom.app X = (Monad.η N).app X
f_μ : ∀ (X : C), (Monad.μ M).app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ (Monad.μ N).app X
⊢ (monadToFunctor C).mapIso (MonadIso.mk f) = f
ext
no goals
case w.w.h
C : Type u₁
inst✝ : Category C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), (Monad.η M).app X ≫ f.hom.app X = (Monad.η N).app X
f_μ : ∀ (X : C), (Monad.μ M).app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ (Monad.μ N).app X
x✝ : C
⊢ ((monadToFunctor C).mapIso (MonadIso.mk f)).hom.app x✝ = f.hom.app x✝
rfl