Theorems · Definition · category theory

CategoryTheory.ComonadIso.mk

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {M N : CategoryTheory.Comonad C} →
      (f : M.toFunctor ≅ N.toFunctor) →
        autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.ε.app X) = M.ε.app X)
            CategoryTheory.ComonadIso.mk._auto_1 →
          autoParam
              (∀ (X : C),
                CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) =
                  CategoryTheory.CategoryStruct.comp (M.δ.app X)
                    (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X))))
              CategoryTheory.ComonadIso.mk._auto_3 →
            (M ≅ N)

Construct a comonad isomorphism from a natural isomorphism of functors where the forward direction is a comonad morphism.

Defined in

Mathlib.CategoryTheory.Monad.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category