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

ETCS axiom 10 witness: power-object lattice completeness. More...

Concept definition

template<typename S>
concept dedekind::category::HasAxiom10PowerObjectLattice =
IsSubobject<S, typename S::Domain> && IsCompatibleSetPair<S, S> &&
requires {
typename S::logic_species;
requires IsOckhamAlgebra<typename S::logic_species>;
}
dedekind::category::HasAxiom10PowerObjectLattice
ETCS axiom 10 witness: power-object lattice completeness.
Definition etcs.cppm:306
dedekind::category::IsCompatibleSetPair
Two set objects over the same ambient species and same Ω codomain.
Definition concrete.cppm:200
dedekind::category::IsOckhamAlgebra
The IsOckhamAlgebra Concept (The Algebraic Signature of Truth).
Definition logic.cppm:114
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 10 witness: power-object lattice completeness.

meet/join/complement on subobjects follows from the subobject classifier (Axiom 7) inducing a Heyting algebra on Sub(A) (Boolean if the topos is Boolean, i.e. L = Boole). The Axiom of Choice proper (every epimorphism splits) is aspirational and not yet encoded here.

etcs__Axiom_10_Power_Object_Lattice

The body requires the carrier to expose its logic_species, verified as an IsOckhamAlgebra: the subobject lattice Sub(A) is INDUCED pointwise from the classifier L (Axiom 7 + Ockham L), so the algebraic witness that L is an Ockham algebra is exactly the power-object-lattice content. The classical-direction Boolean refinement (Diaconescu) lives in the parallel :lattice::IsSubobjectLattice / IsBooleanSubobjectLattice concepts rather than inside Axiom 10's body; see the Diaconescu note below for why.