Formal verification of the directedness axiom: ∀ a, b ∈ T. ∃ c ∈ T. Rel(a, c) ∧ Rel(b, c). More...

Concept definition

template<typename T, typename Rel, typename Ω bool>
concept dedekind::category::IsDirected = 
    IsTruthObject<Ω> &&
    requires(const std::remove_cvref_t<Rel>& rel, const T& a, const T& b) {
      { rel(a, b) } -> std::convertible_to<Ω>;
    } && requires { requires is_directed_v<T, std::remove_cvref_t<Rel>>; }

Detailed Description

Formal verification of the directedness axiom: ∀ a, b ∈ T. ∃ c ∈ T. Rel(a, c) ∧ Rel(b, c).

At the value level, every pair has an upper bound under Rel. Specialised at trait level rather than constructively because exhibiting c for arbitrary a, b in a generic concept body is awkward; the trait specialisation captures the mathematical content for the canonical witnesses (the certified chains: reflexive and connex).