Concept: a set S whose ambient type is std::pair<T1,T2> is a valid binary relation on T1 and T2. More...

Concept definition

template<typename S, typename T1, typename T2>
concept dedekind::relational::IsRelation = 
    dedekind::sets::IsSetObject<S> &&
    dedekind::category::IsProduct<typename S::Domain, T1, T2> &&
    dedekind::category::IsProduct<
        dedekind::sets::universe_t<S>,
        std::remove_cvref_t<𝔸<T1, typename S::logic_species>>,
        std::remove_cvref_t<𝔸<T2, typename S::logic_species>>>

Detailed Description

Concept: a set S whose ambient type is std::pair<T1,T2> is a valid binary relation on T1 and T2.

A relation wears both arrow hats at once (they are not rivals — do not treat one as "the wrong reading"):

as its characteristic function \(\chi_R : A\times B \to \Omega\) it is a callable IsArrow (Domain = pair<A,B>, Codomain = Ω) — this is what R(std::pair{a,b}) evaluates, and it is already an IsArrow today (the subobject-classifier reading);
as \(A \rightsquigarrow B\) it is an allegory arrow, composed by the relative product >> and converse ° of this calculus. The power-transpose adjunction \(\Lambda R : A \to \mathcal{P}(B)\) (apply below) is the bridge: these are one datum viewed three ways. A IsFunction (:graph) additionally collapses the \(\mathcal{P}(B)\) fibre to a single value (a functional + entire relation), so it also reads as the map \(f : A \to B\) — while remaining all of the above.

Note: This concept, IsRelation<S,T1,T2>, is Definition Trsk (§4) made structural: a relation is an Lwv set object (IsSetObject, :boundaries — a subobject of a carrier with χ into a named Ω) whose carrier is the product T1×T2 (IsProduct<Domain,T1,T2>, read through the product's API, whatever spells it) and whose universe is the product of the factor universes, 𝔸 <T1×T2> ≅ 𝔸<T1> × 𝔸<T2> — that last clause is what makes dom / cod below projections (π_1 / π_2 of the universe leg) rather than conventions. It does not encode the arrow implications above: the chain IsLinearOperator ⟹ IsFunction ⟹ IsRelation ⟹ IsArrow is a conceptual reading, reified where needed through the graph adapter (a function's graph IS the IsRelation / IsFunction), not by direct concept subsumption — IsEqualizer and the parallel-pair machinery stay off the concept.

The equalizer reading extends the same conceptual chain: a relation S is a subobject of T1×T2, hence the equalizer of its classifier and ⊤ ( \(\{x \mid \chi_S(x) = \top\}\)); a functional graph \(\Gamma_f\) is moreover the equalizer of the parallel pair \((f\circ\pi_A, \pi_B)\). Like the arrow chain, this is reified through the graph adapter (category::IsEqualizer witnessed on graph(f) and on the affine translation graph, algebra:halfspace_transport, #876), not baked into the concept.