- Generated by
1.15.0
|
Dedekind 0.0.0
A structuralist C++23 Module Library
|
An object of the category Set: a leaf carrying the subobject surface and its legs, or a lattice node — Meet / Join / Not — over set objects on one carrier. The node case is structural: the node's χ is the pointwise evaluation category:lattice already gives it (an arrow into Ω), its universe is its operands', its classifier is the node itself. This is the opaque arm, "the AST is the set", without any set semantics in the lattice partition: the member shape, the inclusion ι and the pullback / pushout apex legs are a sets-side view (as_pullback / as_pushout in :expressions), not a property of the node. The same-logic requirement of the leaf surface is not imposed on nodes: Ø<T,Kleene> ∧ S<T,Boole> is a set object whose reduction the bounded law and the codomain leg decide.
More...
An object of the category Set: a leaf carrying the subobject surface and its legs, or a lattice node — Meet / Join / Not — over set objects on one carrier. The node case is structural: the node's χ is the pointwise evaluation category:lattice already gives it (an arrow into Ω), its universe is its operands', its classifier is the node itself. This is the opaque arm, "the AST is the set", without any set semantics in the lattice partition: the member shape, the inclusion ι and the pullback / pushout apex legs are a sets-side view (as_pullback / as_pushout in :expressions), not a property of the node. The same-logic requirement of the leaf surface is not imposed on nodes: Ø<T,Kleene> ∧ S<T,Boole> is a set object whose reduction the bounded law and the codomain leg decide.
An object of the category Set — a set is \((U, \chi)\): a reified universe and a characteristic map \(\chi : T \to \Omega_L\) into a named logic species.
The model in one sentence: the set is (reified universe, χ); χ's decidable normal forms form a per-carrier, meet-closed coproduct whose discriminant is the only "flag", and everything that escapes it — complements of intervals, cofinite sets, opaque predicates — lives honestly as a term with pointwise χ, where Rice says it must.
This is the mereological / product model recorded on #824 / #826 (the ambient is the whole, χ the part-selector), named as a concept. It is structural and deliberately light — a shape, not a type hierarchy: it refines category::IsSubobject (an object in Set: χ by call shape, the inclusion ι, the domain tie) by requiring the codomain lattice to be a named logic_species with Codomain = logic_species::Ω, the handle through which De Morgan (pointwise, free) and the undecided verdict Unknown reach the set. It is not category::IsSet: that is the category (the ETCS axioms, among them the NNO). The NNO is an axiom of the category, not of an object, so successor is deliberately absent here; and whether == is decidable is a property of the universe's carrier, not a requirement of being a set. SetExpr (:expressions) is the CRTP mixin that realises this surface (Singleton, Halfspace, Interval derive from it); Set realises it by hand.
The two legs are named customization points, universe(s) and classifier(s), found by ADL (every set object lives in, or derives from a mixin in, dedekind::sets, so one default per leg in :boundaries serves them all; a type with better knowledge overloads in its own module). They are deliberately not π_1 / π_2: one object cannot carry two products under the same projection names, and the honest IsProduct here belongs to the universe of a pair carrier, 𝔸 ≅ 𝔸 × 𝔸 (§4: a relation's dom / cod are π_1 / π_2 of its universe), while a lattice node Meet<A,B> is already the product of its operands. Had S itself projected to (universe, χ) through π_1, the universe of a relation could not also project to its factors. The paper's reading survives intact: a set is a subobject of a universe over a regular carrier (Definition Lwv), the predicate is the set, and the universe is the reified type constraint the Python surface hands out.
1.15.0