An arrow E is a regular epi when it is an epi and registered as the coequalizer of some parallel pair. More...

Concept definition

template<typename E>

concept dedekind::category::IsRegularEpi = IsEpicArrow<E> && is_regular_epi_v<E>

dedekind::category::IsEpicArrow

An arrow declared to be an epimorphism (π: A ↠ B).

Definition morphism.cppm:1183

dedekind::category::IsRegularEpi

An arrow E is a regular epi when it is an epi and registered as the coequalizer of some parallel pair...

Definition factorisation.cppm:125

dedekind::category::is_regular_epi_v

constexpr bool is_regular_epi_v

User-declared witness: E is a regular epi (the coequalizer of some parallel pair).

Definition factorisation.cppm:109

Detailed Description

An arrow E is a regular epi when it is an epi and registered as the coequalizer of some parallel pair.

Refines IsEpicArrow by the opt-in regularity witness. Every regular epi is an epi, but not every epi is regular (a textbook foil: in Top, the inclusion of ℚ into ℝ is an epi but not a regular epi). In Set and any topos, every epi is regular.

Form-chain row 4 in the quotient categorification (#718).