dedekind::category::IsLSet Concept Reference

An L-set: a subobject of a carrier with \(\chi : X \to L\) into a named bounded chain \(L\) (Codomain = L::Ω). The carrier is asked for copies (std::semiregular), not for a decidable ==: the equality of sets is the Rice cycle (#970), not a trait of the carrier, so the relations of a hom-set are a carrier too (𝔸<RelExpr>, #1045). An ETCS set asks decidable equality itself (IsSet, whose classifier construction needs it), as IsArrow asks an archetype of its domain rather than a value type (archetype_t). Pst is asked of the species (an Ockham algebra whose Ω is totally ordered), not of the bare Ω, so a Chain<int> set (Ω = int) qualifies while a bare int never does. The chain is the registered total order (IsTotalOrder: reflexive, transitive, antisymmetric, comparable), not the syntactic std::totally_ordered, so an Ω without certified order laws (a raw float, whose NaN breaks reflexivity) is refused honestly. More...

Concept definition

template<typename S>
concept dedekind::category::IsLSet = 
    std::semiregular<typename S::Domain> &&
    IsSubobject<S, typename S::Domain> &&
    requires { typename S::logic_species; } &&
    std::same_as<typename S::Codomain, typename S::logic_species::Ω> &&
    IsOckhamAlgebra<typename S::logic_species> &&
    IsTotalOrder<typename S::logic_species::Ω, std::less_equal<>, bool>

Detailed Description

An L-set: a subobject of a carrier with \(\chi : X \to L\) into a named bounded chain \(L\) (Codomain = L::Ω). The carrier is asked for copies (std::semiregular), not for a decidable ==: the equality of sets is the Rice cycle (#970), not a trait of the carrier, so the relations of a hom-set are a carrier too (𝔸<RelExpr>, #1045). An ETCS set asks decidable equality itself (IsSet, whose classifier construction needs it), as IsArrow asks an archetype of its domain rather than a value type (archetype_t). Pst is asked of the species (an Ockham algebra whose Ω is totally ordered), not of the bare Ω, so a Chain<int> set (Ω = int) qualifies while a bare int never does. The chain is the registered total order (IsTotalOrder: reflexive, transitive, antisymmetric, comparable), not the syntactic std::totally_ordered, so an Ω without certified order laws (a raw float, whose NaN breaks reflexivity) is refused honestly.

topoi__L_Sets

A subobject of a carrier (copies asked, not decidable equality: IsLSet) whose characteristic map lands in a named bounded chain \(L\) is an L-set (Goguen 1967). At \(L = \mathbb{B}\) this is Lawvere's Set, which IsSet refines with the ETCS axioms as implemented here (NNO, well-pointedness, the power-object-lattice approximation of axiom 10; full choice remains aspirational, see HasAxiom10PowerObjectLattice). For a longer chain it is an object of the presheaf topos on the chain — Kleene's \(K_3\) gives the Sierpiński topos, whose Sierpiński object is Rosolini's dominance \(\Sigma\) — which is not well-pointed and has no choice. The paper's \(\mathbf{Lwv}\) set (Definition Lwv) is IsLSet; the Pst fragment is IsFiniteLSet; sets::IsSetObject adds the representation (universe and classifier legs, the structural reading of lattice nodes). The types that satisfy these live downstream in sets and order.

Finiteness is what makes the Pst fragment complete (χ is a finite table; normalisation by evaluation decides equality; the normal form is the family of α-cuts, one run-list per level of \(L\)). Neither IsPst (the truth-object shape: it admits chains of any cardinality and excludes int, which is not IsΩ) nor HasNNOStep (a step; Ternary has none) is that witness, so the fragment is gated on IsFiniteChain: a totally ordered carrier that is finite by its representation — a machine integer or an enumeration. bool, Ternary ( \(K_3\)) and int are the shipped witnesses; ℕ's Cardinality (a variant, unbounded) and the dense carriers are not. Products of finite chains follow with IsProduct.

Template Parameters

S	the candidate set type (Domain, Codomain, logic_species, Member, ι, callable χ).