dedekind::category::HasETCSAxioms Concept Reference

Diaconescu's classical direction (#698 Slice 9 review). More...

Concept definition

template<typename T>
concept dedekind::category::HasETCSAxioms = 
    IsSubobject<T, typename T::Domain> &&
    HasAxiom1Composition<typename T::Domain> &&
    HasAxiom2Identity<typename T::Domain> &&
    HasAxiom3TerminalObject<typename T::Domain> &&
    HasAxiom4WellPointedness<T> &&
    HasAxiom5CartesianProduct<typename T::Domain> &&
    HasAxiom6Exponentiation<typename T::Domain> &&
    HasAxiom7SubobjectClassifier<T> && HasAxiom8EmptySet<typename T::Domain> &&
    HasAxiom9NNO<typename T::Domain> && HasAxiom10PowerObjectLattice<T>

Detailed Description

Diaconescu's classical direction (#698 Slice 9 review).

etcs__Axiom_10_Diaconescu_Note

The standard textbook ETCS Axiom 10 is the Axiom of Choice: every epimorphism splits. Diaconescu (1975) showed that in a topos, AC implies the topos is Boolean (classical internal logic). It is an implication, not a bi-implication: a Boolean topos need not satisfy AC (see etcs__Choice_And_Decidability). The codebase commits to the classifier's side only:

@c L @c = @c Boole @c ⟹ Sub(A) Boolean   (Diaconescu's

classical-Ω direction) L = Kleene ⟹ Sub(A) Heyting (constructive-collapse path)

The Boolean refinement is exposed via the parallel :lattice::IsBooleanSubobjectLattice concept rather than baked into Axiom 10's body. An earlier attempt to gate the conditional inside HasAxiom10PowerObjectLattice triggered instantiation of the set complement, which cascades into default-construction of the capturing-lambda Predicates produced by the comprehension DSL and fails. The parallel-track design avoids that ODR-use cascade; the static asserts in :sets carrier files pin the L-parametric route type-checked at the carrier sites without inducing the cascade.

The reverse direction (Boolean Sub(A) ⟹ full AC) is the splitting-epi witness, which is genuinely aspirational and not yet encoded. The header table's (asp.) marker on row 10 names this remaining gap. Tracked as a separate concept (e.g.\ HasAxiom10AxiomOfChoiceFull) if and when the project commits to it.

Aggregates the 10 ETCS axiom witnesses over a carrier T.

Each axiom is its own concept-level witness (HasAxiom1Composition through HasAxiom10PowerObjectLattice); this concept conjoins them into a single gate. Used by IsSet below as the axioms half of the ETCS set predicate (the other half being the canonical CCC witness over the ambient species).