Category C satisfies the exact-category axioms. Sollbruchstelle landing site. More...

Concept definition

template<typename C>

concept dedekind::category::IsExactCategory = IsSmallCategoryShape<C> && is_exact_category_v<C>

dedekind::category::IsExactCategory

Category C satisfies the exact-category axioms. Sollbruchstelle landing site.

Definition factorisation.cppm:257

dedekind::category::IsSmallCategoryShape

The structural prefix of IsSmallCategory (:small): a type naming an Arrow, a Species and an Id,...

Definition morphism.cppm:253

dedekind::category::is_exact_category_v

constexpr bool is_exact_category_v

User-declared witness: C is an exact category — a regular category in which every equivalence relatio...

Definition factorisation.cppm:241

Detailed Description

Category C satisfies the exact-category axioms. Sollbruchstelle landing site.

Gates on IsSmallCategoryShape<C>; see IsFactorisationSystem above for the rationale.

Set / CanonicalSetCCC and topos-shaped witnesses ship in Slice 2 (the :image rewire), where the necessary downstream imports are already in scope; this slice lands the named seam only.