dedekind::category::IsPredicate Concept Reference

The Predicate Morphism: the DSL's membership test, i.e. the characteristic arrow \(\chi_A : A \to \Omega\). More...

Concept definition

template<typename P>
concept dedekind::category::IsPredicate = 
    IsArrow<P> && !std::same_as<std::remove_cvref_t<P>, bool> &&
    ((IsΩ<Cod<P>> && LogicalMap<P, Dom<P>>) || IsSpeciesTaggedArrow<P>)

Detailed Description

The Predicate Morphism: the DSL's membership test, i.e. the characteristic arrow \(\chi_A : A \to \Omega\).

topoi__Point_Free_Composition_Engine

In the Dedekind topos, a Set is not a container, but a Rule. IsPredicate formalizes this rule as a mapping from a Domain object (T) to a Logical Species (Ω) — an IsArrow whose codomain is a IsΩ (the classifier Ω). This is the named concept for "the membership test"; the two-valued refinement is IsDecidableCharacteristic and the classifier inclusion ι : Σ ↪ Ω is IsDominanceInclusion (both below).

Template Parameters

P	The Predicate candidate (typically a Lambda or a Functor).

@req { p(x) } The candidate must be callable with an instance of the Domain. @req The result type must be a truth-object: either IsΩ<Cod<P>> on its own (it carries the closed logical operators && / || / !, or declares a valid logic_species, e.g. Truth<L>), or the arrow names its species and answers in it (IsSpeciesTaggedArrow: a Chain<int> set answers int, which only its species can vouch for).

Note

By enforcing this contract, dedekind ensures that logical composition (p1 && p2) only occurs between rules that share a common mathematical foundation.