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