dedekind::sequences::SequenceGraph< PathT > Struct Template Reference

as_relation(path) — adapt a Path<T> into its graph relation, a Set of (index, value) pairs. More...

Public Member Functions
template<typename Pair>
constexpr bool	operator() (const Pair &p) const

Public Attributes
PathT	path

Detailed Description

template<typename PathT>
struct dedekind::sequences::SequenceGraph< PathT >

as_relation(path) — adapt a Path<T> into its graph relation, a Set of (index, value) pairs.

path__as_relation_Categorical_Reading

By Bourbaki's function-as-graph definition, a function \(f : \mathbb{N} \to T\) is the set of pairs \(R_f = \{(n, f(n)) \mid n \in \mathbb{N}\} \subseteq \mathbb{N} \times T\) — i.e. a binary relation on std::size_t and T . This adapter exhibits the categorical identity at the type level: for any Path<T, Cardinality> the result is a Set<std::pair<std::size_t, T>, Boole, P> whose predicate P (the graph predicate) tests whether a candidate pair (i, t) belongs to the graph, i.e. whether t == path.at(i) (and, for finite paths, i < path.size() ).

path__as_relation_Why_It_Matters

This is the bridge that makes the §3 (page 2) categorical chain sequence ⟹ set of pairs ⟹ relation a type-checked claim rather than rhetoric. Once a Path<T> is lifted to its relation form, it participates mechanically in the relational-algebra machinery of :sets:relational :

• select returns predicate-defined subobjects (σ in Codd).
• set_union , set_intersection , set_difference act as ∪ , ∩ , ∖ .
• cartesian_product gives × on top of which select(cartesian_product(R, S), θ) reaches the full θ-join of Codd 1970 (Date & Darwen, Third Manifesto ).
• Codd's LIMIT N and its dual are σ-specialisations: spell them inline as select(R, λ(i,t). i < n) (or >= n for the tail), not as named primitives — the same posture as for zip via natural_join .

path__as_relation_Witness

The IsSet witness at the partition boundary asserts that the relation form mechanically satisfies the ETCS Set contract; the categorical identity "a sequence IS a countable set of pairs" is thus type-system-discharged rather than asserted in prose.

The graph predicate of a sequence: (i,t) ∈ graph ⟺ t == seq(i) (within bounds for a finite sequence).

Why a struct rather than a lambda: relation traits (reflexive, symmetric, ...) are registered by type, and a closure type is anonymous. SequenceGraph<PathT> is the named carrier those traits attach to, which is what certifies IsSequence ⟹ IsFunction ⟹ IsRelation.

---

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

• src/main/modules/dedekind/sequences/path.cppm