Commit 2025-11-18 11:33 0939636a

chore(CategoryTheory): IsRegularEpi and its MorphismProperty (#31145) This PR proves that isos are regular epis, and that epis are closed under postcomposition of isos. It also adds IsRegularEpi and the MorphismProperty it induces. This is so we can define regular categories, which require the regular epis to be stable under base change. This is a prerequisite of the MTT project, which aims to use the internal language of toposes to reason about e.g. sheaves.