Commit 2020-11-16 00:17 470ac77c

View on Github →

feat(category_theory/monad): monadic functor really creates limits (#4931) Show that a monadic functor creates_limits, and a partial result for colimits.

Estimated changes

Modified src/category_theory/monad/limits.lean

added def category_theory.monadic_creates_colimits_of_preserves_colimits

added def category_theory.monadic_creates_colimits_of_shape_of_preserves_colimits_of_shape

added def category_theory.monadic_creates_limits

deleted theorem category_theory.monadic_creates_limits