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

Optional naturality witness for Axiom 7 classifier behavior. More...

Concept definition

template<typename S, typename Α, typename F, typename G>
concept dedekind::category::HasAxiom7ClassifierNaturalityWitness =
HasAxiom7SubobjectClassifier<S> && IsNaturalTransformation<Α, F, G> &&
std::same_as<typename F::Σ_cat::Species, typename S::Domain>
dedekind::category::HasAxiom7ClassifierNaturalityWitness
Optional naturality witness for Axiom 7 classifier behavior.
Definition etcs.cppm:196
dedekind::category::HasAxiom7SubobjectClassifier
ETCS axiom 7 witness: every set is represented by a subobject.
Definition etcs.cppm:171
dedekind::category::IsNaturalTransformation
A family of components, one per object, whose square commutes at every arrow of the source: for eac...
Definition natural.cppm:342

Detailed Description

Optional naturality witness for Axiom 7 classifier behavior.

Encodes that classifier-level structure for ambient species A can be paired with a natural-transformation witness over functors rooted in A. This strengthens the proof surface for pullback/reindexing narratives while keeping IsSet backward compatible. This witness is intentionally additive and is not required by IsSet.