Commit 2026-10-17 22:47 4ed598f4

View on Github →

chore(CategoryTheory/Monad): use to_dual (#44628) This PR uses to_dual for Monad/Comonad, and for the Kleisli and Eilenberg Moore categories.

Estimated changes

Modified Mathlib/CategoryTheory/Monad/Algebra.lean

deleted def CategoryTheory.Comonad.Coalgebra.Hom.comp

deleted theorem CategoryTheory.Comonad.Coalgebra.Hom.ext'

deleted def CategoryTheory.Comonad.Coalgebra.Hom.id

modified structure CategoryTheory.Comonad.Coalgebra.Hom

deleted theorem CategoryTheory.Comonad.Coalgebra.comp_eq_comp

deleted theorem CategoryTheory.Comonad.Coalgebra.comp_f

deleted theorem CategoryTheory.Comonad.Coalgebra.id_eq_id

deleted theorem CategoryTheory.Comonad.Coalgebra.id_f

modified def CategoryTheory.Comonad.Coalgebra.isoMk

modified structure CategoryTheory.Comonad.Coalgebra

modified def CategoryTheory.Comonad.adj

deleted theorem CategoryTheory.Comonad.algebra_epi_of_epi

deleted theorem CategoryTheory.Comonad.algebra_mono_of_mono

deleted theorem CategoryTheory.Comonad.coalgebra_iso_of_iso

deleted def CategoryTheory.Comonad.cofree

deleted def CategoryTheory.Comonad.forget

modified structure CategoryTheory.Monad.Algebra.Hom

added def CategoryTheory.Monad.Algebra.adj

added def CategoryTheory.Monad.Algebra.algebraEquivOfIsoMonads

added def CategoryTheory.Monad.Algebra.algebraFunctorOfMonadHom

added def CategoryTheory.Monad.Algebra.algebraFunctorOfMonadHomComp

added def CategoryTheory.Monad.Algebra.algebraFunctorOfMonadHomEq

added def CategoryTheory.Monad.Algebra.algebraFunctorOfMonadHomId

added theorem CategoryTheory.Monad.Algebra.algebra_epi_of_epi

added theorem CategoryTheory.Monad.Algebra.algebra_equiv_of_iso_monads_comp_forget

added theorem CategoryTheory.Monad.Algebra.algebra_iso_of_iso

added theorem CategoryTheory.Monad.Algebra.algebra_mono_of_mono

added def CategoryTheory.Monad.Algebra.forget

added def CategoryTheory.Monad.Algebra.free

modified structure CategoryTheory.Monad.Algebra

deleted def CategoryTheory.Monad.adj

deleted def CategoryTheory.Monad.algebraEquivOfIsoMonads

deleted def CategoryTheory.Monad.algebraFunctorOfMonadHom

deleted def CategoryTheory.Monad.algebraFunctorOfMonadHomComp

deleted def CategoryTheory.Monad.algebraFunctorOfMonadHomEq

deleted def CategoryTheory.Monad.algebraFunctorOfMonadHomId

deleted theorem CategoryTheory.Monad.algebra_epi_of_epi

deleted theorem CategoryTheory.Monad.algebra_equiv_of_iso_monads_comp_forget

deleted theorem CategoryTheory.Monad.algebra_iso_of_iso

deleted theorem CategoryTheory.Monad.algebra_mono_of_mono

deleted def CategoryTheory.Monad.forget

deleted def CategoryTheory.Monad.free

Modified Mathlib/CategoryTheory/Monad/Basic.lean

deleted def CategoryTheory.Comonad.id

deleted theorem CategoryTheory.Comonad.isSplitEpi_iff_isIso_counit

deleted theorem CategoryTheory.Comonad.map_counit_app

deleted def CategoryTheory.Comonad.transport

deleted theorem CategoryTheory.ComonadHom.ext'

deleted theorem CategoryTheory.ComonadHom.id_toNatTrans

deleted def CategoryTheory.ComonadIso.toNatIso

deleted def CategoryTheory.comonadToFunctor

deleted theorem CategoryTheory.comp_toNatTrans

Modified Mathlib/CategoryTheory/Monad/Kleisli.lean

modified def CategoryTheory.Cokleisli.Adjunction.adj

deleted def CategoryTheory.Cokleisli.Adjunction.fromCokleisli

deleted def CategoryTheory.Cokleisli.Adjunction.toCokleisli

deleted def CategoryTheory.Cokleisli.Adjunction.toCokleisliCompFromCokleisliIsoSelf

modified structure CategoryTheory.Cokleisli.Hom

deleted theorem CategoryTheory.Cokleisli.hom_ext

deleted theorem CategoryTheory.Cokleisli.mk_of

deleted theorem CategoryTheory.Cokleisli.of_mk

modified theorem CategoryTheory.Kleisli.mk_of

modified theorem CategoryTheory.Kleisli.of_mk

Modified Mathlib/Tactic/Translate/ToDual.lean