Commit 2025-01-11 13:24 cdcfe3a4
View on Github →chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548)
The names are now prefixed with Is
. As a result, the definition of an abelian category Abelian
only involve props in addition to the Preadditive
instance. With this design, we may avoid diamonds for Abelian
instance in some future works (e.g. the abelian category structure on the heart of a t-structure).