dedekind::relational::Fixed< K, C, c, T > Struct Template Reference

The arrow that fixes one factor of a pair: \(x \mapsto (c, x)\) (K = 1) or \(x \mapsto (x, c)\) (K = 2). Substitution along it is one case of Shannon's expansion. More...

Public Types
using	Domain = T
using	Codomain = std::conditional_t<K == 1, std::pair<C, T>, std::pair<T, C>>

Public Member Functions
constexpr Codomain	operator() (const T &x) const

Detailed Description

template<std::size_t K, typename C, C c, typename T>
requires (K == 1 || K == 2)
struct dedekind::relational::Fixed< K, C, c, T >

The arrow that fixes one factor of a pair: \(x \mapsto (c, x)\) (K = 1) or \(x \mapsto (x, c)\) (K = 2). Substitution along it is one case of Shannon's expansion.

graph__Hyperdoctrine

Quantifiers are the adjoints of substitution (Lawvere). For an arrow \(f : A \to B\) the three operations on subobjects

\[ \exists_f \dashv f^{-1} \dashv \forall_f, \qquad \mathrm{Sub}(A, L) \rightleftarrows \mathrm{Sub}(B, L) \]

are arrows between the objects Subobjects (sets): the pushforward Image, the pullback Preimage (substitution, preimage above), and the dual image Dual \(= \neg\,\exists_f\,\neg\), a composite of three arrows (category::Compose at a presented object). Both adjunctions are witnessed through category::IsGaloisConnection, the arrows carrying their certificates. The pullback is total; the images are partial, defined where the \(\exists\) is eliminated — the Rice wall of the effective domain (dom above) stated as a partial arrow: along an injection (the sum's pushforward, sets::Inject), along the diagonal (diag, the coreflexive), and along a projection whose other factor is a finite chain (Shannon's expansion, the join of the substitutions at each value: the typed twin of the run-time ChainValues). The certificates (monotone, adjoint) are stated once for the whole family, as specialisations of category::monotone_trait / is_adjoint on its pattern: theorems, not tags. Frobenius reciprocity and Beck–Chevalley (#909) are then equations between these arrows, checked below.

Template Parameters

K	the slot the constant takes.
C	the constant's carrier.
c	the constant.
T	the free factor.

---

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

• src/main/modules/dedekind/relational/graph.cppm