dedekind::category::IsSet Concept Reference

ETCS set: a carrier satisfying the 10 ETCS axioms AND admitting the canonical Set-CCC witness over its ambient species. More...

Concept definition

template<typename A>
concept dedekind::category::IsSet = 
    std::regular<typename A::Domain> && IsLSet<A> &&
    std::same_as<typename A::logic_species, Boole> &&  
    HasETCSAxioms<A> && IsCartesianClosed<CanonicalSetCCC<typename A::Domain>>

Detailed Description

ETCS set: a carrier satisfying the 10 ETCS axioms AND admitting the canonical Set-CCC witness over its ambient species.

Conjoins HasETCSAxioms with IsCartesianClosed over CanonicalSetCCC<A::Domain>. Every ETCS category is a CCC — axioms 3 (terminal), 5 (products), 6 (exponentials) are exactly the structural ingredients of a CCC — so the second half of the conjunction is structurally entailed by the first; carrying it in the body makes the CCC guarantee discoverable at the IsSet site rather than per-carrier opt-in. This is the Lambek–Scott payoff: Cartesian-closedness is simply-typed lambda calculus, and the ETCS subset relation lifts that to the typed lambda calculus of the set-builder DSL. Tracked historically under #389.

etcs__ETCS_subset_CCC

Standard categorical fact: every ETCS category is a Cartesian-closed category, but most CCCs are not ETCS. The additional axioms beyond CCC (4 well-pointed, 7 subobject classifier, 9 NNO, 10 choice / power-object lattice) are precisely what fails for general CCCs.

etcs__Regular_carrier

The carrier A::Domain is additionally required to be std::regular: IsSet is the Boolean specialisation of IsLSet, the one place a set's carrier is asked for ==, decidable equality being the diagonal classified in Ω = 𝔹. The algebraic-set concepts sit on IsLSet and ask only std::semiregular (algebra::IsAlgebraOnSet).

Note

std::regular must stay the first conjunct. HasETCSAxioms is not yet a total predicate: on a non-regular domain it is ill-formed (a hard error in the subobject-classifier construction make_χ, which needs decidable equality), not merely unsatisfied. The leading std::regular clause short-circuits to false first, shielding IsSet from that hard error (witnessed in sets/subobject_lattice_carriers_test.cpp). It is asked here, not of every L-set: an L-set's carrier need only have copies (std::semiregular, IsLSet), equality of sets being the Rice cycle. FIXME(#779): make HasETCSAxioms SFINAE-total, after which this ordering becomes defensive rather than load-bearing.

etcs__Choice_And_Decidability

Choice and decidable equality coincide on the sets this library works with, but are distinct axioms:

• Choice implies decidability: in a topos, AC implies excluded middle, so every object's diagonal is complemented (Diaconescu 1975; Goodman and Myhill 1978). ETCS takes choice as an axiom (Lawvere 1964), so an ETCS set has decidable equality.
• The converse fails in general: G-sets for a nontrivial group G form a Boolean topos in which the epimorphism G → 1, G acting on itself, has no section (no point is fixed).
• Over a finite index the converse holds: choosing from finitely many inhabited sets needs no axiom, so a finite, enumerable carrier with decidable equality has choice by search (the enumeration certificate). So choice is not encoded beside == (HasAxiom10ChoiceSplitEpicWitness is opt-in): where a set is finite and decidable it follows, and elsewhere it is a separate certificate. #1116.