The codomain leg of the two-axis reduce (#894). More...

Public Types
using	type = R

Detailed Description

template<typename R>
struct dedekind::sets::codomain_reduce< R >

The codomain leg of the two-axis reduce (#894).

subobject_reduce_t reduces the domain term (the Sub(T) lattice) at a fixed codomain L. This reduces the codomain: a decided boundary factors through the Rosolini dominance \(\Sigma = \{\top,\bot\}\) (its \(\chi\) is the constant \(\bot\) / \(\top\), valued in Σ whatever the ambient), so a normal form that is a boundary carries the Boolean codomain Boole, not the (possibly Kleene) ambient it was reduced under. This is what makes "a structural reduction to @c Ø / @c 𝔸 restores decidability" (see :computability header) actually hold: the collapsed boundary reads HasDecidableMembership.

The single rule for now is boundary → Boole; identity elsewhere. FIXME(#894): the general rule is image(χ) ⊆ Σ folded alongside the domain reduce (the pointwise Kleene image lattice), of which this is the base case. Singleton is deliberately excluded: its decidability needs a decidable == on the carrier (fails on ℝ), so it rides the carrier-axis resolver, not this rule.

The documentation for this struct was generated from the following file:

src/main/modules/dedekind/sets/boundaries.cppm

Public Types

Detailed Description