dedekind::category::arrow_as_relation< F > Struct Template Reference

Adapter: realise an IsArrow F : A → B as a binary relation (a, b) ↦ f(a) == b. More...

Public Types
using	ArrowType = std::remove_cvref_t<F>

Public Member Functions
constexpr bool	operator() (typename ArrowType::Domain const &a, typename ArrowType::Codomain const &b) const

Public Attributes
ArrowType	f

Detailed Description

template<typename F>
requires IsArrow<F> && requires(std::remove_cvref_t<F> const& fn, typename std::remove_cvref_t<F>::Domain const& a, typename std::remove_cvref_t<F>::Codomain const& b) { { fn(a) == b } -> std::convertible_to<bool>; }
struct dedekind::category::arrow_as_relation< F >

Adapter: realise an IsArrow F : A → B as a binary relation (a, b) ↦ f(a) == b.

Bridge between the categorical-arrow reading (in :morphism) and the set-theoretic function-as-relation reading (here in :cartesian, where products are first- class).

Two requirements beyond the bare IsArrow: (1) F must be callable on a const instance — the operator() below is const, so a non-const-callable arrow would not work. (2) F's call result must be equality-comparable with F::Codomain — the relation predicate is f(a) == b. Both are tightened in the requires clause below.

IsArrow itself is a structural shape (it only asserts the call expression is well-formed); it does not guarantee total / law-abiding behaviour over the domain. The opt-in trait specialisations below register left-totality and right-uniqueness on arrow_as_relation by convention — every IsArrow is intended to be a (total, deterministic) function in this codebase. If a carrier ever ships a partial IsArrow (e.g. a wrapper that throws on some inputs), the engineer should un-register the trait on that specific specialisation.

The template parameter F is normalised via std::remove_cvref_t internally, so passing arrow_as_relation<const F> or arrow_as_relation<F&> works the same as arrow_as_relation<F>.

---

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

• src/main/modules/dedekind/category/cartesian.cppm