Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-10 21:44 32b2e305

View on Github →

feat(category_theory/monad): special coequalizers for a monad (#5239) Two important coequalizer diagrams related to a monad

Estimated changes

Created src/category_theory/monad/coequalizer.lean

added def category_theory.monad.beck_algebra_coequalizer

added def category_theory.monad.beck_algebra_cofork

added def category_theory.monad.beck_coequalizer

added def category_theory.monad.beck_cofork

added def category_theory.monad.beck_split_coequalizer

added def category_theory.monad.coequalizer.bottom_map

added theorem category_theory.monad.coequalizer.condition

added def category_theory.monad.coequalizer.top_map

added def category_theory.monad.coequalizer.π