Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::category::IsRegularMono Concept Referenceexport
module dedekind.category

Dual of IsRegularEpi: an arrow M is a regular mono when it is a mono and the equalizer of some parallel pair. More...

Concept definition

template<typename M>
concept dedekind::category::IsRegularMono = IsMonicArrow<M> && is_regular_mono_v<M>
dedekind::category::IsMonicArrow
An arrow declared to be a monomorphism (ι: A ↣ B).
Definition morphism.cppm:1141
dedekind::category::IsRegularMono
Dual of IsRegularEpi: an arrow M is a regular mono when it is a mono and the equalizer of some parall...
Definition factorisation.cppm:143
dedekind::category::is_regular_mono_v
constexpr bool is_regular_mono_v
User-declared witness: M is a regular mono (the equalizer of some parallel pair). Dual to is_regular_...
Definition factorisation.cppm:132

Detailed Description

Dual of IsRegularEpi: an arrow M is a regular mono when it is a mono and the equalizer of some parallel pair.

In Set and any topos, every mono is regular. Form-chain row 5 in the quotient categorification (#718).