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

Structural witness of a split epimorphism e with section s. More...

Concept definition

template<typename Epi, typename Section>
concept dedekind::category::IsSplitEpicPair = IsEpicArrow<Epi> && IsArrow<Section> &&
std::same_as<Dom<Section>, Cod<Epi>> &&
std::same_as<Cod<Section>, Dom<Epi>>
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::IsSplitEpicPair
Structural witness of a split epimorphism e with section s.
Definition etcs.cppm:216
dedekind::category::Cod
typename std::remove_cvref_t< F >::Codomain Cod
Shorthand to look up the Codomain of an Arrow type F.
Definition morphism.cppm:239
dedekind::category::Dom
typename std::remove_cvref_t< F >::Domain Dom
Shorthand to look up the Domain of an Arrow type F.
Definition morphism.cppm:231

Detailed Description

Structural witness of a split epimorphism e with section s.

This concept captures the textbook shape e: A ↠ B and s: B → A. Semantic equations (e ∘ s = id_B) remain a proof obligation supplied by tests or user-declared witnesses.