- Generated by
1.15.0
|
Dedekind 0.0.0
A structuralist C++23 Module Library
|
Structural witness type for an exponential object in the lattice over (T, Rel) viewed as a thin cartesian closed category — the relative complement a → b held as a carrier value, exposed as a callable that computes the eval morphism eval(e, x) = e ∧ x.
More...
Structural witness type for an exponential object in the lattice over (T, Rel) viewed as a thin cartesian closed category — the relative complement a → b held as a carrier value, exposed as a callable that computes the eval morphism eval(e, x) = e ∧ x.
In a Heyting algebra, the exponential object b^a is the value (a → b) ∈ T satisfying the universal adjunction
a ∧ x ≤ b iff x ≤ (a → b).
HeytingExponential<T, Rel> wraps the exponential value and exposes the eval morphism structurally — its operator()(x) computes the meet value ∧ x. The universal property says value ∧ x ≤ b when value = (a → b).
The wrapper satisfies :cartesian::IsExponential<HeytingExponential<T, Rel>, T, T> structurally — eval(e, x) is just the call expression e(x), and the wrapper's operator()(T) returns T. This is the unification across CCCs: function-space exponentials (Set / Cpp) and value-shaped exponentials (Heyting) satisfy the same structural concept body, with no tag declarations or CPO machinery (#698 Slice 6).
The wrapper also exposes Domain / Codomain typedefs, so it satisfies IsArrow when the future IsArrowExponential refinement (#706) lands.
Concrete formulae for canonical carriers:
std::less_equal (with ∧ = min): eval(e, x) = min(value, x). The universal exponential value → b) for input pair top if a ≤ b, else b — derivable from the meet's adjunction.Specialisations beyond the integral / std::less_equal case are tracked under #708.
1.15.0