Def CategoryTheory.Comonad.id

Modification history

2026-10-17 22:47

Mathlib/CategoryTheory/Monad/Basic.lean

chore(CategoryTheory/Monad): use `to_dual` (#44628) …

Deleted CategoryTheory.Comonad.id View on Github →

2023-03-24 13:50

Mathlib/CategoryTheory/Monad/Basic.lean

feat: port CategoryTheory.Monad.Basic (#2969)

Added CategoryTheory.Comonad.id View on Github →