ETCS axiom 4 witness: membership is evaluation through the carrier-as-characteristic-morphism. Post-#681 structural refactor: IsSubobject already requires the structural call shape { s(a) } -> IsΩ, so the membership-as-evaluation reading lands on the IsSubobject witness itself. More...

Concept definition

template<typename S>

concept dedekind::category::HasAxiom4WellPointedness = IsSubobject<S, typename S::Domain>

dedekind::category::HasAxiom4WellPointedness

ETCS axiom 4 witness: membership is evaluation through the carrier-as-characteristic-morphism....

Definition etcs.cppm:156

dedekind::category::IsSubobject

The categorical witness of a monomorphism ι: S ↣ A — a characteristic morphism χ: A → Ω together with...

Definition topoi.cppm:367

Detailed Description

ETCS axiom 4 witness: membership is evaluation through the carrier-as-characteristic-morphism. Post-#681 structural refactor: IsSubobject already requires the structural call shape { s(a) } -> IsΩ, so the membership-as-evaluation reading lands on the IsSubobject witness itself.