dedekind::category::IsExponential Concept Reference

Categorical exponential object B^A — generalised structural recogniser of "eval morphism via call expression" (#698 Slice 6). More...

Concept definition

template<typename E, typename A, typename B>
concept dedekind::category::IsExponential =  requires(E e, A a) {
  { e(a) } -> std::same_as<B>;
}

Detailed Description

Categorical exponential object B^A — generalised structural recogniser of "eval morphism via call expression" (#698 Slice 6).

In a Cartesian closed category C, an exponential object B^A is an object E with an evaluation morphism eval: E × A → B satisfying the currying universal property. The concrete shape of E varies by category:

• Set / Cpp: E is a function-space type (lambda, std::function<B(A)>, std::move_only_function<B(A)>, any callable struct) — the historical reading.
• Heyting algebra (thin CCC): E is a value of the carrier T representing a → b; operator()(x) computes the meet e ∧ x. The universal property says e ∧ a ≤ b.

The unifying observation: in every CCC, the eval morphism is implemented by applying the exponential object to its argument. In C++ that is the call expression e(a). This concept therefore recognises exponentials structurally — by the well-formedness and return type of the call — without committing to function-space representation. Pure Juliet posture: no tag, no CPO, no wrapper- for-tag.

cartesian__Strict_Same_As

The result type is checked via std::same_as, not std::convertible_to. This preserves the Honest Rejection negative witness below (a function returning int does not satisfy IsExponential<…, int, bool>, even though int implicitly converts to bool in C++).

cartesian__Structural_vs_Universal_Property

The concept captures the eval morphism's operational shape (eval(e, a) → B) but does not enforce the currying universal property (∀ f : Γ × A → B, ∃! f̂ : Γ → E). Universal-property enforcement is tracked separately as #707.

cartesian__IsArrow_Harmonisation

IsExponential does not require IsArrow. Function-space inhabitants like std::function<B(A)> satisfy this concept but not IsArrow (no Domain / Codomain typedefs). The project's canonical arrow-shaped exponentials (e.g. outputs of arrow<A, B>(…), HeytingExponential<T, Rel>) satisfy both. The refinement IsArrowExponential = IsExponential && IsArrow is tracked as #706.

cartesian__Slice6_Generalization

Pre-#698-Slice-6 reading was Set-specific: std::move_constructible

• std::invoke_result_t. Slice 6 generalised to the structural call-shape recogniser so that lattice exponentials (Heyting implications, see :lattice::HeytingExponential) participate uniformly. Behavioural preservation: every existing Set-side witness (function-spaces, lambdas, function-objects) continues to fire because being callable with the right signature was already the load-bearing fact under the old definition.