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

A functor that is a regular epi / coequalizer presentation (Borceux Handbook §4.3). More...

Concept definition

template<typename F>
concept dedekind::category::IsQuotientFunctor =
IsArrow<F> && IsEpicArrow<F> && is_quotient_functor_v<F>
dedekind::category::IsArrow
A type that knows its own Domain (A) and Codomain (B), objects it maps between: called at the domain'...
Definition morphism.cppm:168
dedekind::category::IsEpicArrow
An arrow declared to be an epimorphism (π: A ↠ B).
Definition morphism.cppm:1183
dedekind::category::IsQuotientFunctor
A functor that is a regular epi / coequalizer presentation (Borceux Handbook §4.3).
Definition functor.cppm:928
dedekind::category::is_quotient_functor_v
constexpr bool is_quotient_functor_v
Trait registry for the IsQuotientFunctor concept.
Definition functor.cppm:906

Detailed Description

A functor that is a regular epi / coequalizer presentation (Borceux Handbook §4.3).

Quotients are epic in the categorical sense. This concept therefore mechanically requires IsEpicArrow as the textbook structural prerequisite (in addition to the engineer-asserted is_quotient_functor_v trait that pins the stronger regular-epi / coequalizer reading). Categorically dual to IsEmbeddingFunctor: where embeddings are fully-faithful- monic, quotients are coequalizer-epi.

No concrete witnesses today — the slot is reserved for the (A, F) anchor and #602's carrier-lattice quotient half. When witnesses land, each registration site needs both the is_quotient_functor_v specialisation and the underlying is_epic_arrow_v specialisation.