Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
Class Hierarchy

Go to the graphical class hierarchy

This inheritance list is sorted roughly, but not completely, alphabetically:
[detail level 12345]
 Cdedekind::sequences::Ø< T, L >∅: The Initial Object. Extensional (Size 0)
 Cdedekind::sets::Ø< T, L >∅: The Initial Object. Extensional (Size 0)
 Cdedekind::sets::ℵ< N >
 Cdedekind::numbers::𝔸< T, L, C >The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint
 Cdedekind::relational::𝔸< T, L, C >The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint
 Cdedekind::sequences::𝔸< T, L, C >The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint
 Cdedekind::sets::𝔸< T, L, C >The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint
 Cdedekind::algebra::𝔽64The Galois field of order 64, \(\mathrm{GF}(2^6) = \mathbb{F}_2[x] / (x^6 + x + 1)\)
 Cdedekind::category::Acting< H, V, S >An element acting: the arrow \(v \mapsto h(v, s)\) on the set the monoid acts on
 Cdedekind::category::acting_monoid< H >A fold along the walk, fold(r, v, h), and its specialisation by the action law (the Jlt paper's Listing 4). acting_monoid<H> names the monoid an action h acts by on the right, a declared certificate of \(h(h(v, a), b) = h(v, a \cdot b)\) and \(h(v, 1) = v\), the product in the walk's order; keyed by the action's type without cv-qualification, as a fold deduces it. A fold walks a right action; a left action, scalar first as IsLeftAction, is a right action of the opposite monoid and registers Opposite<Op> (:involution), the bridge between the two textbook conventions. On n copies of one value the fold is v acted on by their product, and concat computes the product in one step or by squaring: two declared laws, two overloads, composed by resolution
 Cdedekind::category::acting_monoid< std::plus< std::size_t > >A monoid acts on itself: (std::size_t, +) by +
 Cdedekind::category::ActingOn< H, V, S >The arrows by which a monoid acts on V, as a category: the image of the delooping under the action
 Cdedekind::category::ActionFunctor< H, V, S >A right action as a functor out of the delooping of the monoid it acts by: the one object to V, an element s to \(v \mapsto h(v, s)\). Its functor laws are the action's, \(h(v, 1) = v\) and \(h(h(v, a), b) = h(v, a \cdot b)\), which acting_monoid declares, so they are derived and not declared again. A left action registers the opposite operation, so it is a functor out of the opposite category
 Cdedekind::ieee::AdaptiveErrorPolicy< F >Adaptive policy: respond to risky regions via ternary status
 Cdedekind::category::detail_automaton::AddByteOne more letter of a prefix
 Cdedekind::category::detail_automaton::AddPalindrome< Sigma, N, KL >One more half-site, its word's code a run of one where it lies in the codes kept. Halves ascending give codes ascending, the half being the word's most significant digits
 Cdedekind::category::adjunction_witness< Left, Right, Unit, Counit >Typed unit/counit data for an adjunction witness
 Cdedekind::category::detail_automaton::Advance< Sigma, N, P, K, KL >One pending length of a state's derivative by a letter: the pending words one longer, derived, and the set's own derivative where they are its length, joined; a word of length zero is a match
 Cdedekind::relational::detail_graph::AgreesAt< R, G, A >Whether r and the graph g agree on the pair (a, b)
 Cdedekind::order::detail_cover_witness::AgreesFromFor a fixed a, every b agrees: a < b iff reached
 Cdedekind::order::detail_cover_witness::AgreesOnEvery a in the window agrees with every b
 Cdedekind::category::detail_automaton::AgreesOnPrefixWhether the table and the windows agree on one more prefix
 Cdedekind::relational::detail_graph::AgreesOnRow< R, G, CodRange >Whether r and the graph g agree on every pair of the row a: ∀ b ∈ cod
 Cdedekind::category::detail_periodic::AgreesWithReverse
 Cdedekind::algebra::_has_carrier_witness::algebra_view< T >Thin algebra-view wrapper used as the pilot for the HasCarrier concept (#573) on a primitive carrier
 Cdedekind::sets::detail_setexpr_witness::all_in
 Cdedekind::category::detail_runs::Along< Pred, N, K >One count of a sweep along a predicate: a step where its value changes, nothing where the steps outgrow their bound
 Cdedekind::order::detail_runs::And< L >The species' operations as named functions on L::Ω
 Cdedekind::category::detail_periodic::CycleCount< C, F, T, N >::AndStep< W >One more step's mask into the meet
 Cdedekind::sets::answer_logic< L, Answer >The species of a predicate's answer, relative to the base's species L: an answer already in L::Ω is in L (so a Chain<int> universe accepts an int-valued predicate), otherwise the answer type names its species (classifier_logic_t; no default)
 Cdedekind::sets::answer_logic< L, Answer >
 Cdedekind::category::AnyOperationBase-case sentinel for the operation parameter of IsProduct / IsCoproduct
 Cdedekind::category::detail_periodic::AnyStepThe window's step: whether any is true
 Cdedekind::sets::Ap< F, A >An arrow applied to a term, f(a)
 Cdedekind::relational::detail_rows::AppendColumnsThe step of the fold reading an object's columns off its factors: a leaf's sort; a sum's tag, then its summands' columns
 Cdedekind::relational::detail_rows::AppendLeafThe step of a fold building the factors of a product of carriers: one leaf more
 Cdedekind::ieee::Approx< F >Approximation envelope for an IEEE value
 Cdedekind::category::archetype< C >The representative presentation of an object: itself for a value type; the one it names (C::archetype) otherwise
 Cdedekind::category::archetype< C >
 Cdedekind::category::arrow_as_relation< F >Adapter: realise an IsArrow F : A → B as a binary relation (a, b) ↦ f(a) == b
 Cdedekind::category::ArrowNodeAtThe engine at one former and one law, as a function of the law
 Cdedekind::category::Arrows< T, Op >
 Cdedekind::linear_algebra::Vec2V< T >::ArrowViewNamed-pair view via operator->
 Cdedekind::relational::detail_rows::AsConstant< K >as_constant as a visitor over a row's cells
 Cdedekind::order::detail_interval::AsInterval< V >A piece as the interval it is
 Cdedekind::order::RunListSteps< N, K >::AsStepThe i-th step as the order's: below its position, in where i is even
 Cdedekind::category::detail_arrows::At< T >The visitor that applies the active arrow to x
 Cdedekind::relational::detail_rows::AtDefault< K, Cs >The step of the fold for at_defaults: the column i at its sort's default
 Cdedekind::order::detail_runs::AtLeast< Ω >Whether a value reaches a level, and whether it is the level: the α-cut and the fibre, pointwise
 Cdedekind::category::AtMost< T, K >Words over an alphabet as a tensor, not as a sequence: the tensor power \(\Sigma^n\) of a filtered alphabet, its symmetric sections, and the free monoid on it truncated below a length, each counted as a product of factors that never overflow where the total does. Periodicity above is invariance under a translation of the counts; a symmetry here is invariance under a permutation of the positions of a word
 Cdedekind::algebra::detail_canonical::AtomAt< P, K, Lift >The dispatch of an atom's normal form to its sort: a comparison of two constants decided in it, any other atom in the polynomials over a carrier of the points where + and · are total on it, and on a carrier without them (𝔹, K₃) kept as written: equal forms still cut out equal sets, and different ones decide nothing
 Cdedekind::category::Automaton< Sigma, Q >A matcher's plan: the transitions on each letter, and the states where a word of the set has just been read
 Cjlt::Automaton< Sigma, Q >A matcher's plan: the transitions on each letter, and the states where a word of the set has just been read
 Cdedekind::category::detail_comprehension::Before< Rank, Order >Whether a ranks before b
 Cdedekind::category::Below< C >The coalgebra of the bounded chain [lo, hi]: over the state \(1 + C\), since past hi is no element, and the cover of a saturating top is nothing
 Cdedekind::category::BetaReductionThe β-reduction algebra: a leaf is its own normal form; a node is reduce_β over its reduced legs. reduce_β is a dependent call resolved by ADL against the node type, so a law lives next to its node: the composition unit law above is the canonical exhibit, and further node laws add their own overloads beside their vocabulary. No node carries an is-this-kind tag; dispatch is on the node type
 Cdedekind::sets::Bind< X >The binding algebra at the points X: a constant beside a term (a, b of an operator, a comparison or a conditional) meets the term's carrier now; a constant under an arrow meets the arrow's domain. A leaf binds trivially
 Cdedekind::sets::BindArgs< X >The binding of the arguments of every χ in a body at the points X: each a term bound there, a constant cast into its coordinate's carrier. The body's own binding treats a χ as a leaf, so its arguments are bound here
 Cdedekind::relational::detail_rows::BindMiddle< K >The step of the fold binding a composite's middle: the i-th from the innermost, ∃π_{n + j} over the middle column j = m − i, so the outermost binds the first
 Cdedekind::sets::BinOp< Op, A, B >a op b, the operator a standard functor (std::plus<>, minus, multiplies, divides, modulus) applied in one carrier
 Cdedekind::algebra::Bit2U64ActionScalar action \(\mathbb{F}_2 \times \mathbb{F}_2^{64} \to \mathbb{F}_2^{64}\) on (bool, uint64_t)
 Cdedekind::order::bit_subset_eq< T >Integral carriers under the bitwise Boolean algebra (#710)
 Cdedekind::category::detail_periodic::bit_word< W >The bit word of width W: a machine word where one has the width, std::bitset otherwise
 Cdedekind::category::detail_periodic::bit_word< 16 >
 Cdedekind::category::detail_periodic::bit_word< 32 >
 Cdedekind::category::detail_periodic::bit_word< 64 >
 Cdedekind::category::detail_periodic::bit_word< 8 >
 Cdedekind::linear_algebra::BlockUpperTriangular< A, B, D >Block-upper-triangular matrix — Tier 2 of #366, the degenerate-Schur case where the lower-left block is zero
 Cstd::bool_constant
 Cdedekind::category::BooleThe internal logic of the Classical Topos ({True, False})
 Cdedekind::algebra::BoolLineJoinAdditive join on 1D Boolean vectors (OR)
 Cdedekind::algebra::BoolLineMeetActionScalar action on 1D Boolean vectors via meet (AND)
 Cdedekind::order::Bound< V >One side of an interval as a value: the bound and whether it is attained (non-strict) or not (strict)
 Cdedekind::sets::BoundThe result of a binding: nothing but the checks that ran
 Cdedekind::category::detail_comprehension::bound_of< Coalg >The most elements a walk presents: a take's K, or a bounded list's, kept by each SELECT and WHERE after it (a map presents no more than it reads). No member where nothing bounds the walk
 Cdedekind::category::BoundedAddTransform< T, BoundaryPolicy >Addition that consults a user-supplied numeric boundary policy
 Cdedekind::category::BoundedDivTransform< T, BoundaryPolicy >Division with user-supplied numeric boundary policy
 Cdedekind::category::BoundedMulTransform< T, BoundaryPolicy >Multiplication with user-supplied numeric boundary policy
 Cdedekind::category::Box< T, K, N >The outer product of predicates along chains, \(T(i_1, \ldots, i_K) = f_1(i_1) \wedge \cdots \wedge f_K(i_K)\) over the box of all indices, a rank-one tensor never built: its entry is the legs' Tensor followed by the merge, and the box's sides are the chains' lengths. In the pictures of tensor networks (Bridgeman and Chubb, "Hand-waving and Interpretive Dance: An Introductory Course on Tensor Networks", J. Phys. A 50, 2017), each count contracts a leg's index against a covector: all ones for the box, a residue class for a section
 Cdedekind::category::detail_automaton::Build< Sigma, N, P, K, Q >The construction so far: the states found, in the order found, and the plan's rows for those already walked
 Cdedekind::category::detail_lattice_nodes::BuildsNodesThe opt-in as a leaf property, for over_nodes
 Cdedekind::algebra::detail_polynomial::ByMonomialThe support's order: by monomial
 Cdedekind::category::detail_periodic::ByteAtA position of the bytes as its byte
 Cdedekind::category::detail_periodic::ByteOfA letter as the byte it is: ordered as bytes, not as char, which may be signed. (#1141)
 Cdedekind::category::Bytes< N >A text written in the source: its bytes, held by value, and a view, so a query over it owns them and nothing dangles, a temporary's included. Its copy is constant-time in the sense a view asks, the length being in the type
 Cdedekind::category::canonical_orderThe default Ord: the carrier's own canonical std::less_equal order (the order bundled with its axioms). A caller whose ∧/∨ mean a different lattice on the same carrier injects that relation as Ord
 Cdedekind::relational::CanonicalPairPredicate
 Cdedekind::sets::CardinalityEffectDraft writer-like cardinality effect carrier
 Cdedekind::order::carrier_cardinality< T >Cardinality class of a halfspace's carrier T (#848/#927)
 Cdedekind::order::carrier_cardinality< T >
 Cdedekind::category::carrier_of< X >The carrier type of a reduced term: a value-bearing leaf's ::value type, propagated through Meet / Join composites (a subterm that did not collapse, e.g. Join of two ≤-incomparable elements of a bit-subset lattice), or void when the carrier is unknown (an order-opaque leaf) or inhomogeneous. A composite propagates a carrier only when both children agree on a known one, so a nested mixed-carrier term (at any depth) is void and fails the SameCarrier guard below (fail-closed recursively)
 Cdedekind::category::carrier_of< Join< A, B > >
 Cdedekind::category::carrier_of< Meet< A, B > >
 Cdedekind::category::carrier_of< Not< A > >
 Cdedekind::category::carrier_of< X >Carrier of a predicate / subobject leaf. Such a leaf is an arrow χ:Domain→Ω (IsArrow), not a wrapped value, so its carrier is the arrow's Domain. Reading it through IsArrow (the category arrow surface) rather than a bespoke typedef probe ties the reducer into category. The carrier-based gates (SameCarrier, distributivity, complement, De Morgan negation) then apply to set expressions too. An element leaf instead carries ::value, a point 1→T whose carrier is the value's type; the ::value specialisation above handles it. The two spellings extract the carrier from opposite ends of the arrow, so both coexist
 Cdedekind::sequences::carrier_regime< C, typename >The regime of a carrier for the limit-collapse: Boole when the carrier declares a countable cardinality_type (ℵ_0 / Finite), Kleene when it is uncountable or declares none (the continuum, or a non-cardinality'd primitive such as double). This is a cardinality question (Specker's theorem is about enumerability), not a species one
 Cdedekind::sequences::carrier_regime< C, std::void_t< typename C::cardinality_type > >
 Cdedekind::category::CeilLog2< N >\(\lceil \log_2 \rceil\), the bits a positive count's predecessor occupies: a lax monoid homomorphism \((\mathbb{N}_{>0}, \times) \to (\mathbb{N}, +)\), \(\lceil \log_2 ab \rceil \le \lceil \log_2 a \rceil + \lceil \log_2 b \rceil\), carrying the power action, \(\lceil \log_2 b^e \rceil \le e \lceil \log_2 b \rceil\). The inequality is the soundness of reading a count's width off its factors
 Cdedekind::relational::detail_rows::CellOfSort< Cs >
 Cdedekind::category::Chain< T >Chain<T>: the finite Kleene chain over an integral carrier T, the full-T-range many-valued logic. Boole (2 grades) and Kleene (3) are the small distinguished members; Chain<int> spans the implementation's full int range
 Cdedekind::category::ChainStep< T >One step of the walk: the next value, or the walk itself once it has ended, which makes an ended walk the fixed point iterate stops at
 Cdedekind::sets::ChainValues< K, Lift >The values of a finite chain as constants, through lift: the cases of Shannon's expansion; none for any other carrier
 Cdedekind::category::ChainWalk< T >Where a walk from lo ends: the last value reached and how many values it took. reached_hi says whether it stopped at hi (rather than at a saturating top short of it, or at the end of the budget)
 Cdedekind::numbers::Character< N >The de Moivre CHARACTER \(\chi_m : \mathbb{Z}/N \to \mu_N\), \(k \mapsto \zeta_N^{\,mk}\) — the plane wave "as such", carried SYMBOLICALLY in UnitRoot<N> (consumes the μ_N layer; resolve() collapses to exact ℂ at N=8)
 Cdedekind::category::detail_periodic::CheckedFactor< N >One factor into the product, checked
 Cdedekind::category::detail_periodic::CheckedLength< C, F, N >One length's count into the sum, checked
 Cdedekind::category::detail_periodic::CheckedPlus< N >The checked sum of two exact counts: none if either is none or their sum leaves the word
 Cdedekind::sets::ExtensionalCardinal< W >::CheckedResultA wrapped result and whether the exact result overflowed W
 Cdedekind::sets::SignedExtensionalCardinal< S >::CheckedResultA wrapped result and whether the exact result overflowed
 Cdedekind::sets::ChiTagThe classifier under definition: χ(terms…) in a former's body is the set being formed, applied to the terms
 Cdedekind::category::ClassifierApex< S >The subobject a predicate classifies, as the pullback of the truth \(\top : 1 \to \Omega\) along the predicate \(p : X \to \Omega\) (the subobject classifier's square): its members, the leg into X their inclusion, the leg to 1 the unique one. A view over the subobject, owning nothing
 Cdedekind::category::ClassifierLogic< T >The logic species a classifier answer type belongs to
 Cdedekind::category::ClassifierLogic< bool >
 Cdedekind::category::ClassifierLogic< T >
 Cdedekind::category::ClassifierLogic< Ternary >
 Cdedekind::order::detail_runs::Closed< C >A piece of a discrete chain with ends, read closed: a canonical start is just below its first element, an end just below the element after its last; an absent side at the carrier's end
 Cdedekind::sets::Cmp< R, A, B >The atom a R b over two terms, a relational predicate
 Cdedekind::relational::detail_hyperdoctrine_witness::Code
 Cdedekind::category::codomain_of< X >The CODOMAIN Ω of a leaf / term, dual to carrier_of (the domain). A predicate / subobject leaf is an arrow χ:Domain→Ω, so its codomain is Ω (the subobject classifier), read via ::Codomain. A bare value leaf is a truth value, so its codomain is its own type (domain = codomain there, which is why the two-element bool lattice behaves identically under either accessor). Composites propagate the common Ω (fail-closed, exactly like carrier_of)
 Cdedekind::category::codomain_of< Join< A, B > >
 Cdedekind::category::codomain_of< Meet< A, B > >
 Cdedekind::category::codomain_of< Not< A > >
 Cdedekind::category::codomain_of< X >
 Cdedekind::sets::codomain_reduce< R >The codomain leg of the two-axis reduce (#894)
 Cdedekind::sets::codomain_reduce< Ø< T, L > >
 Cdedekind::sets::codomain_reduce< 𝔸< T, L, C > >
 Cdedekind::category::detail_automaton::ColumnAtOne byte's entry: its rank plus one, or zero
 Cdedekind::linear_algebra::ColumnOrientationTag for column-oriented 1-tensors (vectors in the usual sense)
 Cdedekind::category::ColumnsThe column of a byte in a plan: its rank in the alphabet, as a table of the 256 bytes the compiler computes once, so that a scan does one load per letter where Ranked would count the letters below it. An entry is the rank plus one, zero for a byte outside the alphabet. A Kleisli arrow into Maybe, as Ranked is, and the same arrow by value
 Cdedekind::category::detail_runs::Commutes< P, A, B >The pullback square at one count: the apex holds it exactly where both operands do, and its legs land on the count itself
 Cdedekind::sets::Complement< T, L >The complement as an arrow on the object \(\mathrm{Sub}(T, L)\) (Subobjects, :boundaries), \(S \mapsto \neg S\): an endomorphism, its domain and codomain the one object, presented by every set object over T in L. It is an involution by the reducer's own law \(\neg\neg A \to A\): operator~ peels the node, so ~~s is s, by type, for every presentation s; the certificate reads that law at the representative. The first arrow on sets category::IsInvolution admits: the concept quantifies over the object, not over one value type (morphism__Objects_And_Their_Presentations)
 Cdedekind::linear_algebra::Complex< R >
 Cdedekind::numbers::Complex< R >
 Cdedekind::linear_algebra::detail::ComplexToMatrix2x2Hom
 Cdedekind::category::detail_f_algebra::component_orders< Op >The component orders of a product order, where Op is one
 Cdedekind::category::detail_f_algebra::component_orders< ProductLeq< LA, LB > >
 Cdedekind::category::Compose< F, G >The reified composition arrow g∘f: "apply @c F, then @c G" (diagrammatic f≫g order), the arrow-algebra companion to Identity
 Cdedekind::category::compose
 Cdedekind::category::operations::compose
 Cdedekind::sets::ComposedIsoImagePredicate< SourceSet, FInv >Composed predicate for the iso-decidable image(f, Set) specialisation below: y ↦ S(f^{-1}(y)) where S is the source set's characteristic and f^{-1} is the iso's inverse
 Cdedekind::sets::ComposedRetractImagePredicate< SourceSet, RetractFn, L >Composed predicate for the retract-decidable image(f, Set) specialisation: y ↦ let mx = retract(f)(y); mx.has_value() ? S(mx.value()) : L::False
 Cdedekind::category::ComposePred< PR, PS, B >The composed predicate for the relative product \(R;S\) over a Boolean intermediate, the ∃-over-the-middle enumerated on {false, true}
 Cdedekind::relational::ComposePred< PR, PS, B >The composed predicate for the relative product \(R;S\) over a Boolean intermediate, the ∃-over-the-middle enumerated on {false, true}
 Cdedekind::sequences::ComposePrefixPred< PR, PS >
 Cdedekind::category::composite_functor< F, G >Composite Functor G . F (Maps CatS -> CatT -> CatU)
 Cdedekind::sets::CondSplit< K >A term with its first conditional taken out: the condition, and the term with the conditional replaced by each branch
 Cdedekind::sets::CondT< P, A, B >McCarthy's conditional on terms: a where p holds, else b
 Cdedekind::morphologies::Congruence< N, R >The residue-class predicate \(x \equiv R \pmod N\): the characteristic map of the fiber of the reduction \(\mathbb{Z} \twoheadrightarrow \mathbb{Z}/N\mathbb{Z} =\) Modular<N> over the residue R
 Cdedekind::category::Congruent< N >The residue class \(\{k \mid k \equiv r \pmod m\}\) as a predicate on the counts, periodic with period m: the quotient onto Modular<m>'s carrier, then the test for r
 Cstd::conjunction
 Cdedekind::morphologies::first_iso_mod_2::connectorHand-rolled iso connector Modular<2> → bool
 Cdedekind::morphologies::first_iso_mod_2::connector_invInverse direction: bool → Modular<2>
 Cdedekind::sets::Const< K >A constant, carried as a value
 Cdedekind::sequences::Path< T, Cardinality, Index >::const_iterator
 Cdedekind::linear_algebra::detail_diag::const_rule_six
 Cdedekind::linear_algebra::detail_diag::const_rule_three
 Cdedekind::sets::ConstantAs< P, C, K >A constant read in the sort C: a numeral cast into it, a constant of a sort (a bool, a Ternary) read in its own and embedded
 Cdedekind::category::ConstantMorphism< A, B >The Constant Morphism f: A -> B
 Cdedekind::category::construction_base< D >A carrier's construction: D is built from a base algebra and computes with the base's operations. ::type is the base; ::times_mixes_plus says whether D's × multiplies out (a quotient of a polynomial ring, the Cauchy product: the base's × and +) or stays componentwise (a product, a subalgebra: the base's × alone). Declared once per construction leg in dedekind.algebra (H / P / S / F), never per carrier; a carrier declaring two legs is ambiguous here, honestly
 Cdedekind::category::construction_base< F >
 Cdedekind::category::construction_base< Q >
 Cdedekind::category::construction_base< S >
 Cdedekind::category::detail_periodic::Convolve< N >The cyclic convolution of the histogram so far with one more leg's, in the counts' semiring, the ring of polynomials modulo \(x^m - 1\)
 Cdedekind::category::Copairing< F, G >[f, g] : A + B → C, case analysis out of a sum
 Cdedekind::category::Copy< A >Copy (comonoid comultiplication) Δ:A→A×A, a↦(a,a). The left adjoint of the meet; the fan-out of a cartesian bicategory
 Cdedekind::relational::detail_hyperdoctrine_witness::Copy< A >Copy (comonoid comultiplication) Δ:A→A×A, a↦(a,a). The left adjoint of the meet; the fan-out of a cartesian bicategory
 Cdedekind::relational::CoreflexivePred< S >The coreflexive predicate for \(\Delta_S = \{(x,x) \mid x \in S\}\) — the diagonal restricted to a unary set S (a partial identity): on the diagonal and in S. Carries S by value so it stays inspectable (no lambda)
 Cdedekind::geometry::CotangentBundlePoint< F, N >A point in the cotangent bundle T*(F^N) = F^N × (F^N)*
 Cdedekind::category::counit_witness< Functor, T >Counit_witness<Functor, T>: Generic Kleisli counit witness. Samples a value from the co-Kleisli extension named by Functor::template Shape<T>. Defined for genuine comonadic carriers only; maybe_functor is not specialised here because Maybe is a monad, not a comonad (counit on nullopt has no honest answer)
 Cdedekind::category::counit_witness< dedekind::linear_algebra::matrix2x2_functor< T >, T >Counit / extract for Matrix2x2V<T>: top-left corner. Matches the m11 = (1, 1) entry — the canonical projection from the matrix algebra to the underlying scalar ring
 Cdedekind::category::counit_witness< dedekind::linear_algebra::vec2_functor< T >, T >Counit / extract witness for Vec2V<T>. Canonical projection to the first coordinate; mirrors the Reader-monad π_0 counit
 Cdedekind::category::counit_witness< path_functor< T >, T >
 Cdedekind::category::counit_witness< tuple_functor< T >, T >
 Cdedekind::geometry::CountablyInfiniteDim
 Cdedekind::category::detail_comprehension::CountedThe count of a query, as Maybe's action: a query that may not be, counted where it is
 Cdedekind::category::Counting< J >counting, a counted tensor to its count: the reading that ends a pipeline of arrows, as count ends a query. The cardinality, strong monoidal from \(\otimes\) to \(\times\) (the box law read on counts), modulo the word: a ranking by it is a ranking of the exact counts only while they fit, which the law's plan, evaluating no count, does not need and the fused pass does (#1134)
 Cdedekind::category::counting_action< T, Op >The counts' action on a monoid (T, Op), \((n, x) \mapsto x^n\), the n copies of x, where its laws give it in one step: derived, never declared, and absent where no law gives it, so that the binary method of :total squares instead
 Cdedekind::category::counting_action< T, Op >By the semimodule laws over the counts, \(1 \cdot x = x\) and \((s + t) \cdot x = s \cdot x + t \cdot x\), \(x^n\) is \(n \cdot x\), one action
 Cdedekind::category::detail_comprehension::CountingStage
 Cdedekind::category::detail_periodic::CountOf< L, N >A reading of a factored count, modulo the word: an arrow from the factor lists, with no period of its own; after a periodic sequence, the composite is periodic (period of a Compose)
 Cdedekind::category::detail_periodic::CountStep< N >The window's step: how many are true
 Cdedekind::linear_algebra::covec2_functor< T >
 Cdedekind::linear_algebra::Covec2Map< T, F >f on every entry: the covec2_functor's action on an arrow, an endomap of the entries applied entrywise
 Cdedekind::linear_algebra::Covec2V< T >Value-level row vector (covector) of length 2, viewed as a 1×2 matrix
 Cdedekind::optimization::CriticalPathState< S, Cap >Fold accumulator of annotate: the transient potential net paired with the critical-path predecessor map it induces
 Cdedekind::optimization::CriticalPathStep< S, Cap, CostFn >Fold step of annotate: relax through e and, when the candidate wins the (selective) join, record e.tail as e.head's predecessor
 Cdedekind::category::Curried< T, Op >\(T \to T^T\): the operation, one argument at a time
 Cdedekind::category::detail_automaton::CursorWhere a run of the matcher is: its state and the next position
 Cdedekind::sequences::Curve< Parameter, T, Cardinality >A continuum-indexed family γ: I -> T
 Cdedekind::numbers::Cut< Q >A decidable Dedekind real: a principal rational cut or a rational radical \(\pm\sqrt{c}\)
 Cdedekind::category::detail_periodic::CycleCount< C, F, T, N >The letters that fill a merged cycle of length legs through tau, counted in the bit word of width W: the spider's merge on the truth values is \(\wedge\), so packed it is &, one mask per step around the cycle and one for the letters tau returns, and one popcount
 Cdedekind::category::detail_periodic::CycleFactor< C, F, T, N >One merged leg's factor: the letters that fill a cycle, by popcount in the narrowest word that holds the alphabet, raised to the number of such cycles
 Cdedekind::category::Cycles< N >The cycles of a permutation of positions of one length, and how many there are: one term of its cycle type
 Cdedekind::morphologies::CyclicRing< T, N >Minimal int-backed \(\mathbb{Z}/N\mathbb{Z}\) carrier from the experimental reintegration phase. Retained for parity with the existing test; Modular<N> below is the broader (auto-typed N) replacement
 Cdedekind::category::detail_periodic::CyclicRow< N >One row of a cyclic convolution: residue i of the first histogram against every residue of the second
 Cdedekind::linear_algebra::detail_transfer::CyclicShift
 Cdedekind::category::detail_periodic::CyclicTerm< N >One term of a cyclic convolution: the residues i and j of two histograms add to their sum modulo m
 Cdedekind::category::Cylinder< P, S, N >The words of a tensor power whose window lies in a set of words: the cylinder set \(\pi_I^{-1}(S)\), the legs the window reads constrained by S and every other leg free
 Cdedekind::category::detail_periodic::CylinderFactorsAt< P, S, N >The sequence of a cylinder's factors along the offsets of its window. A power is the same at every position, so every window that fits has the same factors (R2: the offset drops out): period 1, on the offsets where the window fits. The summands of occurrences are this sequence read by CountOf or ExactCountOf
 Cdedekind::category::DaggerFunctor< Dagger, T, Op >A dagger as a functor: from the delooping of (T, Op) to that of its opposite, each element to its dagger. The functor laws are the dagger's, \((a b)^\dagger = b^\dagger a^\dagger\), the composition law into the opposite category, and \(1^\dagger = 1\), which an involutive anti-homomorphism keeps; so they are derived from IsDagger and not declared again. Contravariant on the one object, and its own inverse
 Cdedekind::sets::datum_cardinality< Predicate, Base >
 Cdedekind::sets::datum_cardinality< Predicate, Base >
 Cdedekind::sets::detail::decided< Chi >A classifier read as a decided truth value: its answer converted to bool as if would convert it, so a classifier valued in an explicit truth type (Truth<Boole>) is admitted. Applied as a const value
 Cdedekind::category::detail_automaton::Decode< Sigma, C, P, N >A code read back as its word: the digits in base Sigma, the first letter the most significant, each the letter of that rank
 Cdedekind::sets::default_cardinality< T >Trait behind default_cardinality_t: ℵ_0 for every carrier (the countable fiction of #680) ..
 Cdedekind::sets::default_cardinality< bool >... except bool, which is Finite by its representation
 Cdedekind::algebra::detail_universal::default_signatures< Arrow >The signatures a homomorphism defaults to: the semiring each end of an arrow registers, and the empty signature, which claims nothing, for a type that is no arrow
 Cdedekind::algebra::detail_universal::default_signatures< Arrow >
 Cdedekind::relational::detail_rows::DefineColumn< K, Cs >
 Cdedekind::relational::detail_rows::Defined< K >The columns [lo, hi) as defined by p: per column the term of a conjunct defining it over the columns of others alone, landing in the column's sort (a K₃ term defines no 𝔹 column), and whether nothing else is asked (the residual ⊤). Nothing where a column is not so defined
 Cdedekind::relational::detail_rows::Defining< K >The step of the fold for defined_columns: the terms so far, the predicate left, and whether every column so far was defined
 Cdedekind::sets::Definition< K >A slot's definition: the term t of a conjunct π_slot == t (or t == π_slot) with t free of the slot, and the conjunction without it. ∃π_slot. P is then the rest with t for π_slot: the existential is eliminated by substitution. Dually, under ∀ a disjunct π_slot != t defines it: ∀g. (g ≠ t ∨ Q) ≡ Q[t/g]
 Cdedekind::category::Delete< A >Delete (counit) ε:A→1. Completes the commutative comonoid
 Cdedekind::category::Delooping< T, Op >The delooping \(\mathbf{B}(T, \cdot)\): one object, an arrow per element, composition the operation, the identity its unit. Of the opposite operation, Opposite<Op>, it is the opposite category
 Cdedekind::category::detail_automaton::DeriveSites< Sigma, N, KL >The set's own derivatives, one per letter: the same for every state, so computed once, before the walk
 Cdedekind::sets::DescendsAt< X, J >The measure algebra at the points X for position J: a χ node passes when its argument in position J descends on the coordinate J stands for; every node when all its legs pass; any other leaf vacuously
 Cdedekind::linear_algebra::Diagonal< D, F >Diagonal matrix carrier M: D×D → T parametric in dimension D and diagonal rule F
 Cdedekind::linear_algebra::diagonal_product_rule< F, G >The componentwise rule (F·G)(i) = F(i) · G(i)
 Cdedekind::category::DiagPred< A >The equality-of-coordinates predicate for the diagonal \(\Delta = \{(a,a)\}\). A plain std::equality_comparable check — the diagonal is pure equality, no ordering, so it lives here at the base
 Cdedekind::relational::DiagPred< A >The equality-of-coordinates predicate for the diagonal \(\Delta = \{(a,a)\}\). A plain std::equality_comparable check — the diagonal is pure equality, no ordering, so it lives here at the base
 Cdedekind::category::detail_mereology::Dial< N >A discrete bounded chain of N values that is no enum: a class with a cover step and two bounds, nothing registered about its relations
 Cdedekind::geometry::DifferentiableMap< F, DomainDim, CodomainDim, ValueFn, JacobianFn >A finite-dimensional map paired with a user-supplied Jacobian witness
 Cdedekind::category::detail_automaton::Decode< Sigma, C, P, N >::Digit
 Cdedekind::category::detail_automaton::Decode< Sigma, C, P, N >::Digits
 Cdedekind::linear_algebra::dim_finite< N >Type-level witness for a finite dimension N. Sibling of dedekind::sets::ℵ<N> on the infinite side; together they cover the dimension axis used by Diagonal / OuterProduct without forcing the std::variant<> Cardinality value to appear as an NTTP
 Cdedekind::linear_algebra::DirectSum< A, B >Direct sum of two invertibles — the trivial compositional preserver
 Cdedekind::category::DiscreteCategory< T >DiscreteCategory realization using the Identity Morphism. Lifts a species T into a category where every arrow is the Identity<T>
 Cdedekind::numbers::DiscreteCos< N >The exact discrete COSINE \(\cos_N(k) = \cos(2\pi k/N) = \Re\,\zeta_N^k\) over the Modular<N> angle — the EVEN part of the de Moivre character (= the \(\tfrac12(I+U)\) projection's real value)
 Cdedekind::numbers::DiscreteSin< N >The exact discrete SINE \(\sin_N(k) = \sin(2\pi k/N) = \Im\,\zeta_N^k\) — the ODD part of the character (Im of character<N>(1) resolved). An IsArrow Modular<N> → ℝ, exact at N=8
 Cdedekind::category::detail_lattice_nodes::domain_of< T >The domain of a term, read off its first leaf
 Cdedekind::category::detail_lattice_nodes::domain_of< A >
 Cdedekind::sequences::DominanceRefinement< T, OI, Cost, Order >The dominance-refinement predicate of an argmax: x is optimal iff no member x' of the (finite) domain beats it under order∘cost, i.e. \(\forall x' \in \mathrm{dom}.\ \mathrm{order}(\mathrm{cost}(x'), \mathrm{cost}(x))\). A named functor rather than a capturing lambda, so the refinement is an inspectable type carried in the BoundedSet signature argmax returns — the ∀-filter made visible at compile time
 Cdedekind::category::detail_periodic::Double< N >One step of fast doubling, \((F(j), F(j+1))\) modulo m to \((F(2j), F(2j+1))\) or \((F(2j+1), F(2j+2))\) by bit i of k: \(F(2j) = F(j)(2F(j+1) - F(j))\), \(F(2j+1) = F(j)^2 + F(j+1)^2\)
 Cdedekind::category::detail::DrillDownThe opt-in operator-> drill-down policy: the projector the projected-object concepts take, by name rather than as a lambda
 Cdedekind::analysis::Dual< F >Represents f(x) + f'(x)ε
 Cdedekind::linear_algebra::Dual< F >Represents f(x) + f'(x)ε
 Cdedekind::relational::Dual< F, L >\(\forall_f : \mathrm{Sub}(A, L) \to \mathrm{Sub}(B, L)\), the dual image: \(a \mapsto \{y \mid \forall x.\ f(x) = y \Rightarrow x \in a\}\), which is \(\neg\,\exists_f\,\neg\) (De Morgan: the logic is an Ockham algebra), a composite of three arrows on presented objects. The right adjoint of Preimage; monotone, as anti∘co∘anti
 Cdedekind::linear_algebra::dual_orientation< O >The dual (opposite) orientation — the type-level column↔row flip the transpose / dagger of a 1-tensor performs (a Ket becomes a Bra and vice versa)
 Cdedekind::linear_algebra::dual_orientation< ColumnOrientation >
 Cdedekind::linear_algebra::dual_orientation< RowOrientation >
 Cdedekind::category::detail_periodic::DualIsTheMask
 Cdedekind::linear_algebra::detail::DualToMatrix2x2Hom
 Cdedekind::optimization::EdgeA directed edge of the graph: tail → head (node indices)
 Cdedekind::linear_algebra::detail_transfer::EdgeSuccThe path DAG's edge relation i → i+1, a NAMED predicate carrier (un-lambda'd, so it is a typed relation the DSL converse and relation traits attach to)
 Cdedekind::category::Element< T, Op >A monoid as a category with one object, its delooping, and an action of it as a functor out of that category (Mac Lane, CWM §I.2): the action's laws are the functor's
 Cdedekind::category::detail_comprehension::element_of< E >The value a query's element carries: the Maybe's, or the element itself in a plain sequence
 Cdedekind::category::detail_comprehension::element_of< Maybe< T > >
 Cdedekind::numbers::EmbedRationalToReal< I >The field embedding \(\mathbb{Q}\hookrightarrow\mathbb{R} =\mathbb{Q}(\sqrt2)\), \(q\mapsto q+0\sqrt2\)
 Cdedekind::sets::EmbedsAt< P >Whether the sort b embeds into the sort a, at points of P
 Cdedekind::sets::EmptyPredicate< T >The empty predicate: rejects every element of T
 Cdedekind::relational::detail_rows::Encoded< K >The step of the fold for encodes: the predicate so far and the slot reached; a leaf moves one slot on, a sum asks that its tag pick a side and moves past its columns
 Cdedekind::relational::detail_rows::EncodeFactor< K, Cs >
 Cdedekind::category::detail_automaton::EndsInSiteThe kernel the table factors: whether a prefix ends in a word of the set, reading its last six letters and nothing kept
 Cdedekind::category::detail_automaton::EndsInSubsetThe kernel the random words' table factors
 Cdedekind::sets::Env< T, R >The point and the set under definition, threaded through a body: the term nodes read it as the point (conversion, and term_value below), Self reads it as the set
 Cdedekind::category::Equals< A >The equality test against one value as an arrow \(A \to 2\), the characteristic map of the point x: the condition a guard asks of a state (the Jlt paper's Listing 3, until(equals(1), step))
 Cdedekind::order::detail_runs::EqualTo< Ω >
 Cdedekind::sets::EuclideanDivision
 Cdedekind::category::_factorisation_upgrade_witnesses::exact_category_witnessCategory-shape-tagged toy carrier for upgrade-chain witnesses
 Cdedekind::category::detail_periodic::ExactCountOf< L, N >A reading of a factored count, exactly: as CountOf
 Cstd::exceptionSTL class
 Cdedekind::category::detail_comprehension::Extended< F >A Kleisli arrow into Maybe extended to the elements of a query, \(\kappa(-, f) : \mathit{Maybe}\,A \to \mathit{Maybe}\,B\)
 Cdedekind::category::detail_kleisli::Extending< Step >A fold step on \(T(A)\): the step at the element, by κ
 Cdedekind::sets::ExtensionalCardinal< W >Finite extensional cardinal: one machine word W
 Cdedekind::sets::ExtensionalSet< T, L, Hash, Equal >
 Cdedekind::category::f_algebra< Carrier, Functor, Structure >A concrete witness for an F-algebra
 Cdedekind::category::f_coalgebra< Carrier, Functor, Structure >A concrete witness for an F-coalgebra
 Cdedekind::category::Factor< N >A factor of a count, \(b^e\): a base raised to an exponent
 Cdedekind::relational::FactorA factor of an object: a carrier (a leaf, its sort the column's), or the sum \(X + Y\) of two objects (#1039). A sum lays out a tag column (𝔹: which summand), then the left summand's columns, then the right's; a row reads only the active side, so every column keeps one carrier
 Cjlt::Factor< N >A factor of a count, \(b^e\): a base raised to an exponent
 Cdedekind::category::detail_periodic::factor_word< T >The count word of a factor
 Cdedekind::category::detail_periodic::factor_word< Factor< N > >
 Cdedekind::category::detail_periodic::FallsAlong< T >One more letter of the alphabet against the one before it: the map's images must not rise along the chain of the letters
 Cstd::false_type
 Cdedekind::category::FibonacciMod< N >The Fibonacci numbers modulo m, \(k \mapsto F(k) \bmod m\), by fast doubling, \(\log k\) steps; the modulus is at most the square root of the word's order, so that the products stay in the word, and a wider one is refused where the arrow is read
 Cdedekind::relational::FibrePredicate< Rel, T1 >The reified fibre of a relation R at a point x: the predicate \(b \mapsto (x,b)\in R\). Named (the sibling of GraphPredicate / PreimagePredicate) so the fibre is stable and inspectable rather than a lambda blackbox (#840)
 Cdedekind::sets::FieldDivisionThe two divisions Python tells apart, as keys: a field's, and the Euclidean one of an ordered carrier with remainder. The typed grammar's std::divides<> is the carrier's own, admitted where either is
 Cdedekind::sets::Finite
 Cdedekind::geometry::FiniteDim
 Cdedekind::optimization::FiniteNet< X, Cap >A finite net: a tabulated morphism size_t → X (an IsNet, since std::size_t is a directed set). Read as a function d(v); the std::array tabulation is private business, not the interface
 Cdedekind::sequences::FiniteNet< X, Cap >A finite net: a tabulated morphism size_t → X (an IsNet, since std::size_t is a directed set). Read as a function d(v); the std::array tabulation is private business, not the interface
 Cdedekind::optimization::FiniteSeq< T, Cap >A finite sequence: an array-backed range of length n ≤ Cap — the compile-time extensional realization of a sequence
 Cdedekind::sequences::FiniteSeq< T, Cap >A finite sequence: an array-backed range of length n ≤ Cap — the compile-time extensional realization of a sequence
 Cdedekind::sets::Verdict< P, K >::FiniteSortWhether a sort is a finite chain, enumerated exactly
 Cdedekind::relational::detail_rows::FirstSet< N >The step of a fold for the first index whose flag is set: the answer so far, or N while there is none
 Cdedekind::category::detail_periodic::FixByteOne byte into the identity table
 Cdedekind::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
 Cdedekind::category::FixedBy< P, S, T >fixed_by(g), a tensor power to its section fixed by g, a permutation of the positions after a letter map on every letter: an arrow between tensors. By Pólya each cycle of g fills with the letters it fixes, at most \(|\Sigma|^{\ell}\) for a cycle of length \(\ell\), so the section's density is at most 1. The section is the equalizer \(\mathrm{Eq}(\mathrm{id}, g)\) (IsEqualizer, :pullback), equally the limit of the action of \(\langle g \rangle\) on the power, a functor out of its delooping (ActionFunctor, Delooping, :functor): its invariants, Pólya their count
 Cdedekind::category::detail_periodic::FixedByReflectedReversefixed_by(~rev) before it meets the powers it applies to
 Cdedekind::category::detail_periodic::FixedByStage< S, T >fixed_by(g) before it meets the powers it applies to
 Cdedekind::order::detail_runs::FoldPieces< Op, L >The species' fold of the values over the carrier's own pieces: a step before every element sets the first value, one after every element ends the fold
 Cdedekind::sets::detail_terms_witness::Foreign
 Cdedekind::category::free_algebra_base< F >free_algebra_base<F>: carrier-side declaration that F is the free algebra over some base R (the textbook companion to HSP; cf. Burris–Sankappanavar §II.11). Specialise the ::type member at the carrier-defining partition (e.g. Polynomial<R, M> in algebra:polynomial records free_algebra_base<Polynomial<R, M>>::type = R)
 Cdedekind::category::free_algebra_base< dedekind::algebra::Polynomial< R, M > >
 Cdedekind::category::FreeMonoid< C, F, N >The free monoid on a filtered alphabet, truncated below a length: \(\Sigma^{<L} = \coprod_{n < L} \Sigma^n\), the coproduct of the tensor powers, concatenation of words its operation
 Cjlt::FreeMonoid< C, F, N >The free monoid on a filtered alphabet, truncated below a length: \(\Sigma^{<L} = \coprod_{n < L} \Sigma^n\), the coproduct of the tensor powers, concatenation of words its operation
 Cdedekind::sets::EmbedsAt< P >::From< A >
 Cdedekind::order::detail_runs::Front
 Cdedekind::category::FullMachineBoundaryPolicy< T >Full-machine boundary policy (no clipping)
 Cdedekind::geometry::FunctionalVector< F, Fn >A vector-like object defined by coordinate evaluation x[i]
 Cdedekind::category::functor_of< MA >The functor whose values a container is: Maybe a value of maybe_functor , the one-tuple of tuple_functor . Kleisli extension reads its action on arrows, \(\mu \circ T(f)\)
 Cdedekind::category::functor_of< Maybe< A > >
 Cdedekind::category::functor_of< std::tuple< A > >
 Cdedekind::algebra::GaloisFieldRegistration
 Cdedekind::analysis::GaussianKernel< T >Gaussian radial basis function (RBF) kernel
 Cdedekind::category::GetLogic< T >The logic a thing lives in, with Boole as the permissive default: a type that names no logic_species and is not a known answer type is read as classical. IsTotalArrow asks this of a plain carrier (an int domain is classical). Do not use it to read the species off a classifier answer: that is classifier_logic_t, which has no default and rejects an answer type that names no species
 Cdedekind::category::GetLogic< std::optional< T > >
 Cdedekind::category::GetLogic< T >
 Cdedekind::category::GetLogic< Ternary >
 Cdedekind::relational::GraphArrow< A, B, P >The arrow a function's graph atom names, the converse of graph: a relation A×B | (π_2 == t) certified a function is the arrow a ↦ t(a), t read at a pair whose first coordinate is a
 Cdedekind::relational::GraphPredicate< F >The membership predicate of a functional graph \(\Gamma_f\): \((a,b)\mapsto b = f(a)\)
 Cdedekind::optimization::Halfspace2D< T, a, b, c >2D halfspace a·x + b·y ≤ c, entries as NTTPs
 Cdedekind::optimization::Halfspace2DPredicate< T, a, b, c >:expressions predicate for one 2D halfspace a·x + b·y ≤ c
 Cdedekind::optimization::HalfspaceTriple< T >Value-level halfspace carrier (a, b, c) for the bridge kernel. Paired with the NTTP carrier Halfspace2D: an instance of Halfspace2D<T, a, b, c> destructures into a HalfspaceTriple <T>{a, b, c} for the uniform value-vector the kernel consumes. The two structures share one role — the halfspace — split across the type/value boundary the bridge straddles
 Cdedekind::category::detail_kleisli::HalvedA witness's step that may fail: half of an even count
 Cdedekind::analysis::HarmonicOscillator< R >Concrete Hamiltonian carrier for the 1-D harmonic oscillator
 Cdedekind::category::HeytingExponential< T, Rel, Meet >Structural witness type for an exponential object in the lattice over (T, Rel) viewed as a thin cartesian closed category — the relative complement a → b held as a carrier value, exposed as a callable that computes the eval morphism eval(e, x) = e ∧ x
 Cdedekind::category::HeytingExponential< T, dedekind::order::bit_subset_eq< T >, std::bit_and< T > >HeytingExponential specialisation for the bitwise Boolean lattice (#710): on integral T (excluding bool — see caveat below) under bit_subset_eq with std::bit_and as meet, the relative complement a → b = ~a | b (Boolean Heyting), and the eval morphism e(x) = e & x (meet). Required so IsHeytingLatticeCategory fires at row 6 of the Form-chain for this Rel / Meet pairing
 Cdedekind::category::HeytingExponential< T, std::less_equal< T >, Inf >Canonical specialisation: integral carriers under std::less_equal with Inf as the meet. Holds an exponential value value ∈ T; operator()(x) returns Inf(value, x), the lattice meet, which is the eval morphism in a thin Heyting algebra
 Cdedekind::category::Symmetric< P, S, T >::Holds< V >One position of a word against the condition: the letter at i is the power's, and its image under tau is at sigma(i)
 Cdedekind::numbers::HonestDivRational< I >Division transform for Rational
 Cdedekind::category::HonestDivTransform< T >Division with truncation-awareness (Ternary Logic)
 Cdedekind::category::horizontal_composition< Α, Β, F, F_prime, G, G_prime >Horizontal composition (Godement product)
 Cdedekind::relational::detail_rows::Identify< K >The step of the fold for identified: one equation more
 Cdedekind::category::Identity< T >The Identity Morphism and Functorial Witness
 Cdedekind::category::identity_functor< Cat >
 Cdedekind::category::identity_monad_tag
 Cdedekind::linear_algebra::identity_rule< T >Identity rule: i ↦ T{1}. IsArrow witness for the constant unit
 Cdedekind::category::identity_transformation< F >The Identity Natural Transformation for Functor F
 Cdedekind::category::IdentityIn< Cat >The identity of a category whose arrows are one type, Cat::Arrow: an identity arrow on Cat::Species, so its law is read at the type, that converts to the category's arrow, Cat::unit_arrow(), where an arrow of that type is wanted
 Cdedekind::order::IdentitySteps< C >χ(x) = x on a finite chain, valued in the chain's own species: a step at every element above the least (none on a one-element chain)
 Cdedekind::ieee::IEEE< F >IEEE effect wrapper: values interpreted under machine IEEE semantics
 Cdedekind::ieee::IEEEAdd< F >Certified operation token for addition under IEEE-by-fiat semantics
 Cdedekind::ieee::IEEEMul< F >Certified operation token for multiplication under IEEE-by-fiat semantics
 Cdedekind::order::detail_runs::Iff< L >a ⇔ b in the species: both, or neither
 Cdedekind::ieee::IgnoreErrorPolicy< F >Ignore policy: run fast lane and drop all diagnostics
 Cdedekind::relational::Image< F, L >\(\exists_f : \mathrm{Sub}(A, L) \to \mathrm{Sub}(B, L)\), the image along \(f : A \to B\): \(a \mapsto f[a] = \{f(x) \mid x \in a\}\). Partial: defined where image_along eliminates the \(\exists\). Monotone; the left adjoint of Preimage
 Cdedekind::category::image_carrier< F >Opt-in trait: textbook claim "for this @c F, @c im(F) is the carrier @c ::type"
 Cdedekind::category::image_carrier< dedekind::morphologies::first_iso_mod_2::mod_2_arrow >
 Cdedekind::category::detail_morphism::image_of< F, T >The carrier a map on T lands in: an arrow's declared codomain, a bare callable's result
 Cdedekind::category::detail_morphism::image_of< F, T >
 Cdedekind::category::ImageChi< F >The characteristic predicate of image_of(F) — recognises y as "in the image of @c F"
 Cdedekind::category::ImageChi< F >Image classifier for a retractable arrow: y is in the image iff the retract fires at y
 Cdedekind::category::In< N >The NNO's structure map \([Z, S] : 1 + N \to N\) as an arrow: zero, or the successor of the element given. std::optional<N> is \(1 + N\), the NNO's own functor \(F(X) = 1 + X\)
 Cdedekind::category::detail_arrows_witness::Inc
 Cdedekind::category::InfMeet ∧: the greatest lower bound on a chain (min), returned by value. Value-returning sibling of Sup
 Cdedekind::category::infer_morphism< F, Args >Universal inference for any Morphism signature f: Args... -> Codomain
 Cdedekind::category::infer_morphism< F, A >
 Cdedekind::category::infer_morphism< F, A, A >
 Cdedekind::category::infer_morphism< std::bit_and< T >, T, T >
 Cdedekind::category::infer_morphism< std::bit_or< T >, T, T >
 Cdedekind::category::infer_morphism< std::divides< T >, T, T >
 Cdedekind::category::infer_morphism< std::equal_to< bool >, bool, bool >
 Cdedekind::category::infer_morphism< std::less< T >, T, T >
 Cdedekind::category::infer_morphism< std::less_equal< T >, T, T >
 Cdedekind::category::infer_morphism< std::logical_and< bool >, bool, bool >
 Cdedekind::category::infer_morphism< std::logical_or< bool >, bool, bool >
 Cdedekind::category::infer_morphism< std::minus< T >, T, T >
 Cdedekind::category::infer_morphism< std::multiplies< T >, T, T >
 Cdedekind::category::infer_morphism< std::plus< T >, T, T >
 Cdedekind::category::detail::InitialEnvelope
 Cdedekind::sets::InitialObjectArrow< Init, Target >InitialObjectArrow<Init, Target> — the unique arrow from the initial object into any subobject (Init → Target), i.e. the empty function / the ⊥-of-Sub(U) leg. Dual to inclusion_arrow: where that reifies an inclusion into the ambient, this reifies the initiality mediator out of Ø. Gated on category::IsInitialObject<Init> so only a genuine initial object (Ø, tagged) can be the source; the body forwards the (vacuous) Member value and is unreachable in practice (Ø has no members). Canonical span leg for a pushout A ← Ø → B, replacing hand-rolled per-instance span structs. #881
 Cdedekind::relational::detail_hyperdoctrine_witness::Inject< K, UA, UB >\(\exists_{\iota_K}\): a set of the summand as the set of the sum that is it on its summand and empty on the other, kept as a sum (the strength reduction a | Ø → a is the inverse direction). The left adjoint of Restrict
 Cdedekind::sets::Inject< K, UA, UB >\(\exists_{\iota_K}\): a set of the summand as the set of the sum that is it on its summand and empty on the other, kept as a sum (the strength reduction a | Ø → a is the inverse direction). The left adjoint of Restrict
 Cdedekind::category::Injection< K, A, B >The injection ι_K : A → A + B as an arrow: monic (it is injective, and its image is disjoint from the other summand's), the ground of a sum's strength reduction (a set inside one injection's image pulls back along it without loss)
 Cdedekind::relational::detail_hyperdoctrine_witness::Injection< K, A, B >The injection ι_K : A → A + B as an arrow: monic (it is injective, and its image is disjoint from the other summand's), the ground of a sum's strength reduction (a set inside one injection's image pulls back along it without loss)
 Cdedekind::category::Injections< A, B >The injections of the coproduct std::variant<A, B> as a named operation (IsCoproduct's Op, #881): inl / inr place a value by index, so equal summands stay apart (variant<int, int>). Static members, as the concept asks for Op::inl(a) / Op::inr(b)
 Cdedekind::sets::detail_sum_witness::Injections< A, B >The injections of the coproduct std::variant<A, B> as a named operation (IsCoproduct's Op, #881): inl / inr place a value by index, so equal summands stay apart (variant<int, int>). Static members, as the concept asks for Op::inl(a) / Op::inr(b)
 Cdedekind::sets::detail::insert_intoThe step of the folds below: insert one element into the container accumulated so far, and hand it on (Rule 3: a fold, not a loop). The element is taken by value and moved in, so a transformed result is moved, not copied (a move-only one included)
 Cdedekind::order::InSlot< I, S >\(\pi_I^{-1}(S)\): the cylinder of a set S on axis I of a pair, a relational predicate
 Cdedekind::category::detail_quotient::IntByEquality
 Cstd::integral_constant
 Cstd::integral_constant< std::size_t,(N<=std::numeric_limits< std::size_t >::max()) ? static_cast< std::size_t >(N) :std::size_t{0}>
 Cstd::integral_constant< std::size_t,(std::numeric_limits< T >::digits< std::numeric_limits< std::size_t >::digits) ?(std::size_t{1}<< std::numeric_limits< T >::digits) :std::size_t{0}>
 Cdedekind::relational::Intersect< R, S, Meet >The point-free composite meet R∩S = Δ† ∘ (R⊗S) ∘ Δ: copy the shared domain, run both legs in parallel, merge their codomain outputs where they agree. The arrow-level (spider) realisation of the relational intersection, whose (Copy,Merge) legs are certified by IsMeetAsRightAdjoint — the same R∩S the extensional operator& above computes over Set<pair>, spelled point-free
 Cdedekind::category::IntervalBoundaryPolicy< T >Closed interval policy [lower, upper] for integral species
 Cdedekind::algebra::Inverse< G, Op >The group inverse under Op, reified as an arrow (an endomorphism G → G)
 Cdedekind::category::inverse_trait< T, Op >The Formal Trait: Hooks the bridge into the Concept system
 Cdedekind::category::inverse_trait< dedekind::analysis::Dual< F >, std::plus< dedekind::analysis::Dual< F > > >
 Cdedekind::category::inverse_trait< dedekind::linear_algebra::Covec2V< T >, std::plus< dedekind::linear_algebra::Covec2V< T > > >
 Cdedekind::category::inverse_trait< dedekind::linear_algebra::Vec2V< T >, std::plus< dedekind::linear_algebra::Vec2V< T > > >
 Cdedekind::category::inverse_trait< dedekind::numbers::Complex< R >, std::multiplies< dedekind::numbers::Complex< R > > >
 Cdedekind::category::inverse_trait< dedekind::numbers::Complex< R >, std::plus< dedekind::numbers::Complex< R > > >
 Cdedekind::category::inverse_trait< dedekind::numbers::QuadraticReal< D, Q >, std::plus< dedekind::numbers::QuadraticReal< D, Q > > >
 Cdedekind::category::inverse_trait< dedekind::numbers::Rational< I >, std::plus< dedekind::numbers::Rational< I > > >
 Cdedekind::category::inverse_trait< dedekind::numbers::UnitRoot< N >, std::multiplies< dedekind::numbers::UnitRoot< N > > >
 Cdedekind::category::inverse_trait< SC, std::plus< SC > >
 Cdedekind::category::inverse_trait< T, Op >
 Cdedekind::category::inverse_trait< Z1, std::plus< Z1 > >
 Cdedekind::linear_algebra::Invertible2x2< T, a, b, c, d >Full-rank 2×2 matrix with entries as non-type template parameters
 Cdedekind::sequences::detail::IotaBounds< T >The [start, bound) iota_view bounds a finite value set normalises to (shared between to_iota_view and from_iota_view): the Interval / Singleton / Empty kinds of a Interval, read off its value endpoints. An unbounded kind (Halfspace / Universe) has no finite range and yields the empty bounds; a per-arm overload will refuse it once the set is a coproduct (#970)
 Cdedekind::sequences::IotaIntersectionstd::ranges::iota_view as a Form-chain object: an order::IsOrderMeetSemilattice under subset-inclusion, with intersection as the meet
 Cdedekind::category::detail_periodic::IsEmptyFactor< N >Whether a factor is empty, \(0^e\) with \(e > 0\)
 Cdedekind::category::detail_periodic::IsLetterAtWhether a position of the bytes is a letter
 Cdedekind::sequences::detail_relprod::IsMiddle< PR, PS, Pair >Whether b is a middle for \((a, c)\): \(R(a,b) \wedge S(b,c)\), with b the i-th element of ℕ
 Cdedekind::category::IsoRetract< F >The retract of an IsIsomorphism: its total inverse arrow wrapped in an always-engaged std::optional
 Cdedekind::category::IsSquare< W >A pattern of even width length, packed into the bit word of width W, that is a square \(u u\): fixed by the rotation by half its width, within its width, the padding apart. For a width \(2^k\) these are exactly the proper powers, the patterns that are not primitive (Lothaire, Combinatorics on Words, §1.3): every proper divisor of \(2^k\) divides \(2^{k-1}\)
 Cdedekind::category::detail_chain_arrows::IsZero
 Cdedekind::category::detail_periodic::Iterate< T, N >A letter after tau taken steps times
 Cdedekind::category::unfold_view< S, Coalg >::iteratorA position of the walk: the element, the next state, live
 Cdedekind::order::MergeView< RA, RB, F, V, L >::iterator
 Cdedekind::order::PiecesView< R, V >::iterator
 Cdedekind::category::detail_periodic::Iverson< N >The Iverson bracket, bool to the counts, a semiring map
 Cdedekind::category::Join< A, B >
 Cdedekind::category::Join< A, B >
 Cdedekind::category::join_logic< L1, L2 >The join of two species: the least shipped species both embed into. Partial: comparable species join to the larger one; an incomparable pair (K₃ / Chain<int>, across the parity gap) has no shipped upper bound and no type, so a cross-species combine of such sets is refused at compile time rather than mis-typed. HaveLogicJoin asks whether the join exists
 Cdedekind::category::join_logic< L1, L2 >
 Cdedekind::category::JoinWith< P, S >join_with(p), a set of words to its join with p on the window: the join curried in the set, an arrow between tensors, its exponential transpose (curry, :cartesian); each join the pullback along the window (IsPullback, :pullback)
 Cdedekind::category::detail_comprehension::JoinWithStage< P >
 Cdedekind::relational::detail_rows::Keep
 Cdedekind::category::detail_comprehension::KeepBest< T, K, Rank, Order >One more element into the best K so far, sorted by the rank: inserted after those it does not rank before, so ties keep the walk's order, and the last cut where the list overflows. O(K) on the stack
 Cdedekind::category::detail_periodic::KeepInSliceOne more byte, kept where the slice and the predicate both do
 Cdedekind::category::detail_comprehension::KeepsWhatItClassifies
 Cdedekind::relational::detail_rows::KeptThe step of the fold checking a projection's columns: each in 1 … n and none twice. seen has n + 1 slots
 Cdedekind::category::detail_periodic::KeptAfter< F, T, N >Whether the letter tau takes steps times to is kept
 Cdedekind::category::kernel_quotient< F >Opt-in trait: textbook claim "for this @c F, @c A/ker(F) is the carrier @c ::Class"
 Cdedekind::category::kernel_quotient< dedekind::morphologies::first_iso_mod_2::mod_2_arrow >
 Cdedekind::category::detail_comprehension::KernelAt< T, K >The kernel at one more prefix
 Cdedekind::category::KleeneThe internal logic of the Kleene Topos
 Cdedekind::category::kleisli_probe_arrow< A, B >An arrow A → B the triple concepts probe bind and extend with: only its type is read, never its value. In this namespace, not a detail one, so argument-dependent lookup finds the >>= and <<= defined below
 Cdedekind::sequences::lasso_presentation< Seq >Opt-in finite-state ("lasso") presentation of an eventually-periodic sequence: a prefix of length pre_period followed by a cycle of length period (s(n) = s(n+period) for all n ≥ pre_period). The primary carries no presentation; a witness specialises it with the finite (pre_period, period) data — the engineer's honesty obligation (the presentation cannot be computed in general). Absorptive ⇒ period = 1; periodic ⇒ pre_period = 0
 Cdedekind::category::LastOf< T >The history comonad's counit: a prefix's last letter
 Cdedekind::order::detail_runs::LastValueThe value of the later step: a fold that keeps the last one
 Cdedekind::category::lattice_less_logic< Less >The logic species a comparator reports in: Boole (a bool decision) unless the comparator names its own logic typedef (e.g. Kleene, so an undecidable comparison can be Unknown)
 Cdedekind::category::lattice_less_logic< Less >
 Cdedekind::category::LatticeBottom< T, Rel >Structural witness types for the bottom (initial) and top (terminal) of the lattice over (T, Rel), playing the role of initial / terminal objects of the lattice viewed as a thin category
 Cdedekind::category::LatticeBottom< T, dedekind::order::bit_subset_eq< T > >Bitwise-lattice bottom: the all-zeros bitmask
 Cdedekind::category::LatticeBottom< T, std::less_equal< T > >Canonical specialisation: integral carriers under std::less_equal have bottom = numeric_limits<T>::min()
 Cdedekind::geometry::LatticeFactory< S >Factory for unbounded lattice discretizations by set species
 Cdedekind::numbers::LatticeFactory< AmbientSet, N >Primary template for lattice factory values
 Cdedekind::numbers::LatticeFactory< ℝ_d, 1 >Lattice factory specialization for ℝ
 Cdedekind::numbers::LatticeFactory< ℝ_d, N >Lattice factory specialization for ℝ^N, N > 1
 Cdedekind::geometry::LatticeFactory< 𝔸< I > >
 Cdedekind::geometry::LatticeFactory< NaturalLatticeSet >
 Cdedekind::category::LatticeTop< T, Rel >The abstract top of the lattice over (T, Rel), dually
 Cdedekind::category::LatticeTop< T, dedekind::order::bit_subset_eq< T > >Bitwise-lattice top: the all-ones bitmask
 Cdedekind::category::LatticeTop< T, std::less_equal< T > >Canonical specialisation: integral carriers under std::less_equal have top = numeric_limits<T>::max()
 Cdedekind::category::law_inactiveSentinel: a law that does not fire on the given node
 Cdedekind::category::LawAlgebra< Op >The law algebra: a leaf is its declared profile, a node the law engine on its legs' profiles (:posetal, arrow_node); any other node certifies nothing (sound). The second algebra for the same cata: BetaReduction lands in a normal form (a free algebra, so it decides equality), LawAlgebra in a finite domain of profiles (an abstract interpretation, so it certifies, sound, not complete)
 Cdedekind::relational::LawSet< Re, W >The relations certified the law W: a datum on the universe of relations, so 𝔸<Re>{} & Total<Re>{} is the set of total relations, membership its χ in K₃ (inferred, or not), and a map or an isomorphism a meet of such sets, nothing stored. Its χ obeys the facts the set is declared: closed under >>, so S(f) ∧ S(g) ≤ S(f >> g); a down-set or an up-set in ⊆; carried by ° to its dagger law. Its complement is never inhabited by inference (¬True, else Unknown): Σ, not Π
 Cdedekind::category::detail_automaton::LawsOnSeed
 Cdedekind::category::LeftActing< Act, M, S >A scalar acting on the left: the arrow \(m \mapsto s \cdot m\) of a semimodule
 Cdedekind::category::LeftActingOn< M, S, AddM, AddS, MultS, Act >The arrows by which the scalars act on a semimodule, as a category: certified by the semimodule's laws, so its identity is the scalars' unit
 Cdedekind::category::LeftActionFunctor< M, S, AddM, AddS, MultS, Act >A semimodule's left action as a functor out of the opposite of the delooping of its scalars' product: \((s t) m = s (t m)\), so s then t along the walk acts as \(t s\), the opposite product, and \(1 m = m\) keeps the identity. Those laws are the semimodule's, which is_linear_action declares, so the functor laws are derived. A left action of a monoid is a right action of its opposite: the right actions are ActionFunctor
 Cdedekind::category::Length< N >len(n): the fibre of the length over n, the predicate a graded family of words is met with. oligos & len(n) is the words of length n, \(\Sigma^n\) as the fibre of \(\Sigma^* \to \mathbb{N}\) over n, Trsk's filter on the graded set; it is the family applied at n, so the count law of the fibre is the power's, \(|\Sigma|^n\). The meets commute: oligos & len(n) & fixed_by(g) and oligos & fixed_by(g) & len(n) are one section
 Cdedekind::category::detail_comprehension::LengthOfA kernel for the laws: a prefix's length
 Cdedekind::category::detail_automaton::Letter< Sigma, N, P, K, KL, Q >One letter out of the state being walked: its derivative's number, a new state numbered next where it is new
 Cdedekind::category::LetterMapAn arrow on the bytes given by a table, each letter of from to the letter at the same place of to, every other byte fixed: letter_map("ACGT", "TGCA") is the complement of a base, an involution
 Cjlt::LetterMapAn arrow on the bytes given by a table, each letter of from to the letter at the same place of to, every other byte fixed: letter_map("ACGT", "TGCA") is the complement of a base, an involution
 Cdedekind::category::LetterMapsThe letter maps on the bytes as a category: one arrow type, LetterMap, the identity its identity table
 Cdedekind::category::LetterMapsOnWordsThe letter maps on every letter of a word as a category: the image of LetterMaps under the list functor
 Cdedekind::category::LettersA subobject of the bytes given by its letters, \(\chi : \Sigma \to \Omega\) as a packed word of 256 bits: the predicate a filtered alphabet is built from, letters("ACGT")
 Cjlt::LettersA subobject of the bytes given by its letters, \(\chi : \Sigma \to \Omega\) as a packed word of 256 bits: the predicate a filtered alphabet is built from, letters("ACGT")
 Cdedekind::category::Lifted< Op >A fold step lifted through Maybe: Maybe's eliminator with the cases \([\mathit{acc}, \mathit{op}(\mathit{acc}, \cdot)]\), a hole leaving the accumulator as it is. Written once, so the folds that end a query take their plain steps and none cases on a hole
 Cdedekind::order::detail_runs::LiftInto< J >A value lifted along the dominance into the species J
 Cdedekind::category::LiftLogic< L >The arrow reading of the Rosolini dominance inclusion \(\iota:\mathbb{B}\hookrightarrow\Omega\) (lift_logic): a decided bool answer embeds as the target species' poles (⊥↦False, ⊤↦True). The canonical order-PRESERVING arrow, and the covariant codomain axis of a classifier \(\chi:A\to\Omega\) (#908)
 Cdedekind::linear_algebra::detail_diag::linear_rule_int
 Cdedekind::optimization::LinearFunctional< T, cx_, cy_ >Linear functional U : F → T with NTTP-typed coefficients. Carries the objective as type parameters so argmax can call the NTTP-driven implementation detail::maximize_set directly without smuggling the values through function parameters
 Cdedekind::geometry::LinearMap< F, Rows, Cols >A dense compile-time-sized linear map F^Cols -> F^Rows
 Cdedekind::category::logic_complement< L >Bridge the species' static-method ops (L::AND / L::OR / L::RFL) to the function-object types the :species / :total law registry is keyed on
 Cdedekind::category::LogicTraits< T >Primary Template: Default to Classical (Boolean) Logic
 Cdedekind::category::LogicTraits< T >Specialization for Floating-Point Species (IEEE 754 NaN handling)
 Cdedekind::numbers::LowerCut< Q >The datum of a real's lower set: the real itself, χ(q) = real.contains(q)
 Cdedekind::optimization::LPSolutionPredicate< T >:expressions predicate carrying the LP's runtime optimal locus as (point, feasible) value-level state
 Cdedekind::category::MakeJoinThe pairing factory for the join (∨, pushout): ⟨-,-⟩ : A×B→Join
 Cdedekind::category::MakeMeetThe pairing factory for the meet (∧, pullback): ⟨-,-⟩ : A×B→Meet
 Cdedekind::category::detail_periodic::MapByteOne letter and its image into a table on the bytes
 Cdedekind::category::Mapped< S, Coalg, F >The functor's action on a coalgebra: f on the emitted leg
 Cdedekind::order::detail_runs::MapSteps< V, L >A sorted map of breakpoints as a source
 Cdedekind::order::detail_runs::MapValue< F, L2 >A step with its value mapped into the species L2
 Cdedekind::category::Matches< Sigma, Q >matches(plan), the stage that runs a matcher along a text: a query over the text's positions, present where a word of the plan's set ends
 Cdedekind::category::detail_automaton::MatchStep< Sigma, Q, V >One position of the run: the state after its letter, and the position itself where that state accepts. O(1) state, the text read where it is
 Cdedekind::linear_algebra::MatNxNV< S, N >Mat(S): the N×N matrix over a semiring S. Entries are stored row-major; ⊕ / ⊗ are S's semiring operations, read off dedekind::algebra::semiring_ops (never native operator+/*, which the tropical carriers skew)
 Cdedekind::linear_algebra::MatPlus< S, N >Mat(S)'s additive monoid ⊕: elementwise base-⊕
 Cdedekind::linear_algebra::Matrix2x2< T, a, b, c, d >General (possibly-singular) 2×2 matrix with NTTP entries
 Cdedekind::linear_algebra::matrix2x2_functor< T >
 Cdedekind::linear_algebra::Matrix2x2Map< T, F >f on every entry: the matrix2x2_functor's action on an arrow, an endomap of the entries applied entrywise
 Cdedekind::linear_algebra::Matrix2x2V< T >Value-level 2×2 matrix — the runtime companion to NTTP Matrix2x2
 Cdedekind::linear_algebra::MatTimes< S, N >Mat(S)'s multiplicative monoid ⊗: the ⊕-⊗ contraction c_{ij} = ⊕_k a_{ik} ⊗ b_{kj} (matrix multiply)
 Cdedekind::category::maybe_functor< T >The Intensional Functor for Optional (Maybe) values
 Cdedekind::category::maybe_monad_tag
 Cdedekind::category::MaybeMap< T, F >f on the value an optional holds, none where it holds none: the optional functor's action on an arrow. Its codomain is stated, so an arrow into optionals lifts to one into optionals of optionals, as a Kleisli extension needs, and is never collapsed by deduction
 Cdedekind::category::Meet< A, B >
 Cdedekind::category::Meet< A, B >
 Cdedekind::category::meet_logic< L1, L2 >The meet of two species: the greatest species embedding into both. Total: 𝔹 (the dominance Σ) embeds into every species, so the order is a meet-semilattice with 𝔹 at the bottom. Comparable species meet at the smaller one; an incomparable shipped pair meets at 𝔹 (their only common lower bound). The meet is relative to the registered edges: two even chains (Chain<int>, Chain<long>) meet at 𝔹 here although an embedding between them exists mathematically; register the edge to refine it. A new species that shares a non-𝔹 lower bound with a species it does not compare to must specialise this
 Cdedekind::category::meet_logic< L1, L2 >
 Cdedekind::category::detail_etcs_total_witness::SetOverNonRegular::Member
 Cdedekind::category::PullbackApex< Apex, A, B >::MemberA member of the apex: one value, read in each operand. Its components are the legs, Π<1, Member> and Π<2, Member> as arrows (:limit's projections), the co-restrictions A ∧ B ↪ A and A ∧ B ↪ B: inclusions, so monic, not epic
 Cdedekind::category::PushoutApex< Apex, A, B >::Member
 Cdedekind::category::RunList< N, K >::MemberThe subobject surface: a member is a count the run list holds, and its inclusion into the counts is the count itself
 Cdedekind::category::Subobject< A, Chi >::MemberThe Internal Member of the Subobject. Wraps a value from the ambient space that satisfies the classifier
 Cdedekind::numbers::𝔸< T, L, C >::MemberMember-shape mirror of Subobject's: every element of T is a member of U via the always-True classifier; the wrapper carries the T-value the IsSubobject contract reads back through ι
 Cdedekind::relational::𝔸< T, L, C >::MemberMember-shape mirror of Subobject's: every element of T is a member of U via the always-True classifier; the wrapper carries the T-value the IsSubobject contract reads back through ι
 Cdedekind::relational::RelExpr< K, Cs >::Member
 Cdedekind::sequences::Ø< T, L >::MemberMember-shape mirror of Subobject's. Vacuously inhabited (Ø has no members) — but the wrapper type is still required so the IsSubobject contract has a Member-to-T projection to read through ι
 Cdedekind::sequences::𝔸< T, L, C >::MemberMember-shape mirror of Subobject's: every element of T is a member of U via the always-True classifier; the wrapper carries the T-value the IsSubobject contract reads back through ι
 Cdedekind::sets::Ø< T, L >::MemberMember-shape mirror of Subobject's. Vacuously inhabited (Ø has no members) — but the wrapper type is still required so the IsSubobject contract has a Member-to-T projection to read through ι
 Cdedekind::sets::𝔸< T, L, C >::MemberMember-shape mirror of Subobject's: every element of T is a member of U via the always-True classifier; the wrapper carries the T-value the IsSubobject contract reads back through ι
 Cdedekind::sets::SetExpr< Derived, DomainT, L >::MemberA member is a carrier value; ι projects it back into the ambient (the subobject inclusion the ETCS axioms read)
 Cdedekind::sets::MentionsSelfThe self algebra: a term or predicate mentions the set under definition when one of its leaves is a χ node; every node passes it up
 Cdedekind::category::detail::merc_filtered
 Cdedekind::category::detail::merc_shell
 Cdedekind::category::Merge< A, Meet >Merge (the dagger of copy) Δ†:A×A→A, (a,b)↦a⊓b. The right adjoint of the diagonal; the value that IsMeetAsRightAdjoint certifies as the glb
 Cdedekind::category::MergeBadOp
 Cdedekind::order::MergeSteps< A, B, F >Two sources merged along the chain under a pointwise operation: the steps of both, each read as f of the two values there
 Cdedekind::category::detail_automaton::MirrorDigit< Sigma, N >One more digit of a half-site read backwards, reflected: the next letter of the other half, \(\sigma - 1 - d\) on the ranks
 Cdedekind::morphologies::first_iso_mod_2::mod_2_arrowThe parity homomorphism mod_2: int → bool
 Cdedekind::morphologies::Modular< N >\(\mathbb{Z}/N\mathbb{Z}\) as a total finite cyclic ring
 Cdedekind::morphologies::ModularCongruence< N >The binary congruence relation \(x \equiv y \pmod N\) on the integer carrier: the kernel of the reduction \(\mathbb{Z} \twoheadrightarrow \mathbb{Z}/N\mathbb{Z} =\) Modular<N>
 Cdedekind::algebra::Monomial< N >A monomial in N variables: its exponents, one per slot (π is the slot 0; π_1, π_2, π_3 the slots 1, 2, 3). The free commutative monoid on N generators, written multiplicatively (the exponents add, as natural numbers: leaving the word raises), and a chain under the graded lexicographic order: by total degree, then by exponents
 Cdedekind::category::MorphicBridge< T >
 Cdedekind::category::MorphicBridge< R(C::*)(A) const >
 Cdedekind::category::MorphicBridge< R(C::*)(A)>
 Cdedekind::category::MorphicBridge< std::function< R(A)> >
 Cdedekind::category::MorphicBridge< T >
 Cdedekind::category::Morphism< A, B, Func >The formal structure of an Arrow f: A -> B
 Cdedekind::category::Morphisms< T, Op >
 Cdedekind::category::NaNHolePolicy< T >IEEE-754 NaN-hole classifier policy for floating species
 Cdedekind::sets::NaZ
 Cdedekind::category::NegationArrow< L >The arrow reading of logic negation ¬ = L::RFL on the truth object Ω — the canonical order-reversing arrow
 Cdedekind::sets::NegativeInfinity
 Cdedekind::category::detail_automaton::NextByteOne more byte of a word: its rank, the next digit
 Cdedekind::category::no_canonical_orderNo order for the reducer to canonicalise by: a carrier without one keeps the residue in its authored order, then combines it
 Cdedekind::category::no_leaf_combineThe default leaf-combiner performs no domain combination. Two order-incomparable leaves stay a Meet / Join node. A downstream carrier (e.g. sets) injects a Combine that computes the actual domain meet / join of two compatible leaves. structured_and of two halfspaces yields an Interval, say. Combine returns law_inactive when no domain combination applies. This injected policy lets the reducer's incomparable-leaf residual fall through to the carrier's own ∧/∨
 Cdedekind::sets::NoConstantsNo carrier value as a constant: the lift that names nothing, so eliminate_quantifiers eliminates by definition alone and leaves every quantifier over a chain to the search
 Cdedekind::relational::NodeAtThe engine at one node and one law, as a function of the law; the converse reads its operand at the dagger law
 Cdedekind::category::detail_etcs_total_witness::NonRegular
 Cdedekind::category::Not< A >
 Cdedekind::category::Not< A >¬A over an arrow A → Ω is the arrow RFL ∘ A: the codomain's own reflection (generic over any bounded chain Ω: Boole !, Kleene ¬U=U, …). The node stays the literal Not , so is_not_node_v / de_morgan_of / is_complement_pair_v apply unchanged; its set-object reading is structural, downstream in sets
 Cdedekind::order::detail_runs::NotAfterAllA step inside or below the carrier: the fold ends at the first one above every element
 Cdedekind::order::detail_runs::NotPast< V >A step at or before x: its position is not past x
 Cdedekind::category::NumericWitness< T >A typed witness of numeric classification in Ω_K3
 Cdedekind::relational::ObjectAn object: a product of factors in normal form, a list. The product is associative with unit 1 (the empty list), so \((A \times B) \times C\) and \(A \times (B \times C)\) are the same object by construction, and >> composes regardless of grouping. Read as a binary tree, (first, rest), where a tree is asked for (kind / operands in Python). The columns are its factors'
 Cdedekind::category::Offsets< N >The offsets a window takes, as a tensor: the chain of m, its count m, one factor \(m^1\). Its outer product with a tensor is the copower \(m \cdot X\), m copies, the action of \(\mathbb{N}\) on the counts (:action; Listing 4's concat on copies). Fubini's sum over the offsets, every summand the same (period 1, translation invariance), is this factor of the product
 Cdedekind::order::detail_connective::OfKind< K >Whether a predicate is of the kind k (a bound to fold)
 Cdedekind::sets::On< C >The carrier a rule is stated for, as a tag. A rule admits(On<C>, key, divisor_is_constant) says that the operator key is in the signature of C: a symbol one of the carrier's certified varieties has. It is declared in this namespace beside the certificate and found by ADL, so it is in force where that module is imported: the comparisons beside the partial orders (order:poset), // and % beside IsDividableChain (order:completeness), a field's / beside IsField (algebra:field); + - * and == != here, whose certificates are category's. Without a rule an operator is not in the signature
 Cdedekind::category::detail_comprehension::OneAn element's share of a take: one if present, none for a hole, read through Maybe's eliminator
 Cdedekind::linear_algebra::one_hot< T, D >The one-hot / basis vector e_k : j ↦ δ(j,k) = [j=k] (T{1} on its own index k, T{0} elsewhere) — a 1-arg IsArrow, the k-th COLUMN of the identity Identity (the Kronecker δ with one leg fixed; Diagonal 's entry is δ_ij·F)
 Cdedekind::algebra::OneDimensionalVector< S, Tag >Reified carrier for a 1D module/vector-space coordinate
 Cdedekind::analysis::OneForm< F, N >The cotangent vector (The 'Gradient' components)
 Cdedekind::category::OnWords< S >A transformation of the power functor with one component, a map on the words, the same at every letter
 Cdedekind::category::Opaque< F >An arrow with its laws hidden: called as f, with no period, so that a count along it is the plain fold. What a test runs beside the law to check it
 Cdedekind::order::detail_steps::OpaqueNot a step source: a leaf the run lists do not read (an opaque predicate), or a node over one
 Cdedekind::category::detail_involution::opposite< Op >
 Cdedekind::category::detail_involution::opposite< Reversed< Op > >
 Cdedekind::order::detail_runs::Or< L >
 Cdedekind::category::OrderBy< Rank, Order >order_by(rank), SQL's ORDER BY: the stage that sorts a query by rank under Order, a strict weak order on the ranks. Ties are SQL's: which of the tied elements a take keeps, and in which order, is the plan's (a law's rewrite reads them in the walk's order or its reversal, the fused pass in the walk's); a rank without ties orders alike under every plan
 Cdedekind::category::origin_trait< T >Primary trait: The distinguished 'Point' of a species
 Cdedekind::category::origin_trait< T >Atomic Proof: Integrals are pointed at 0
 Cdedekind::category::Outer< A, B >An outer product of two counted tensors, its count the product of theirs
 Cdedekind::linear_algebra::OuterProduct< U, V, Mult >Rank-1 matrix M = u⊗v with M[i][j] = u(i)⊗v(j), the product taken in a semiring
 Cdedekind::category::Pack< W >A pattern, given by its count, in the bit word of width W, the padding above it zero: the switch of representation, from the counts to the word whose API has the rotations and masks. A section of unpack on the counts below \(2^W\)
 Cdedekind::category::Pairing< F, G >⟨f, g⟩ : A → B × C, one argument into a product
 Cdedekind::category::PairwisePred< Op >A binary predicate on A read at the pair ⟨a, b⟩: the other direction of the bridge a set over a product crosses (#1047), so std::less_equal<bool> is a set of pairs. Named, so it carries op and the set inherits every law op has on A (the rules below)
 Cdedekind::relational::PairwisePred< Op >A binary predicate on A read at the pair ⟨a, b⟩: the other direction of the bridge a set over a product crosses (#1047), so std::less_equal<bool> is a set of pairs. Named, so it carries op and the set inherits every law op has on A (the rules below)
 Cdedekind::category::Partial< T >The Kleisli Context for "Consistently Broken" Species
 Cdedekind::numbers::PartialAddComplex< R >Partial addition transform for Complex<R>
 Cdedekind::numbers::PartialAddRational< I >Partial addition transform for Rational
 Cdedekind::numbers::PartialEmbedIntegerToRational< I >Identity and Associativity traits for Rational arithmetic
 Cdedekind::numbers::PartialMulComplex< R >Partial multiplication transform for Complex<R>
 Cdedekind::numbers::PartialMulRational< I >Partial multiplication transform for Rational
 Cdedekind::sequences::Path< T, Cardinality, Index >A sequence F: ℕ → T
 Cdedekind::sequences::Path< N >
 Cdedekind::sequences::Path< Ternary >
 Cdedekind::category::path_functor< T >The path functor for the Path <·> shape (#508 / PR #521 review)
 Cdedekind::category::detail_comprehension::Pending< Q, Rank, Order >order_by without a law to read, pending its take: it needs the whole query, so only the fused order_by >> take<K> is offered, never the sort alone (it would need the caller's buffer)
 Cdedekind::category::PercentThe bounded confidence chain: a 101-grade De Morgan (Kleene) chain, self-dual about 50
 Cdedekind::category::PercentagePercentage: a range-enforcing [0,100] carrier ("50:50")
 Cdedekind::order::Piece< V >A piece on which a two-valued source holds: a start (nullopt below every element) and an end (nullopt above)
 Cdedekind::sets::PinConstant< K, Lift >A numeral read in the sort C and written back as a constant of that sort, through lift; a carrier lift has no constant for keeps the numeral
 Cdedekind::category::detail_periodic::Pisano< N >One step of the search for the Pisano period: the pair \((F(j), F(j+1))\) modulo m, and the least j at which it is \((0, 1)\) again, once found
 Cdedekind::category::detail_periodic::PlusLogPower< N >One factor into the width: its power's image under CeilLog2, \(e \lceil \log_2 b \rceil\), added saturating, the \((\mathbb{N}, +)\) side of TimesPower's fold
 Cdedekind::sets::Point< T >
 Cdedekind::sets::point_sorts< P >The sorts of a point type: the carriers of its coordinates, each once. A carrier value has one sort; a pair of two carriers two (one where they agree). A term built at run time names no carrier until it is bound, and every node then has a sort: a projection its slot's, a constant its context's, an operator its operands' common one, a comparison 𝔹
 Cdedekind::sets::point_sorts< Row< Cs... > >
 Cdedekind::sets::point_sorts< std::pair< A, B > >
 Cdedekind::linear_algebra::PointwiseSum< F, G, Add >The pointwise ⊕ of two arrows over a shared domain: \((f \boxplus g)(x) = f(x) \oplus g(x)\). An IsArrow (the sum vector)
 Cdedekind::algebra::Poly< C, N >The polynomial reading of a term on the carrier C, an algebra for cata: a projection is its variable, a constant a coefficient, + - * the polynomial's where the carrier admits them, a division by a nonzero constant on a field the multiplication by its inverse. Any other node (//, %, a division by a term, an applied arrow, a conditional) has no free algebra catalogued here and is refused. Expanding into polynomials uses commutativity of * and its distributivity over +, so the carrier must be a certified commutative rig
 Cdedekind::algebra::Polynomial< R, M >The monoid algebra R[M]: a finitely supported function from the monomials to the coefficients, stored as its support sorted along the monomials' chain, no coefficient zero. A net (Domain the monomials, Codomain the coefficients, p(m) the coefficient of m), a commutative rig over a commutative rig, a ring over a ring (- where R has additive inverses)
 Cdedekind::optimization::Polytope2D< T, cx, cy, Hs >Polytope context: the (cx, cy, Hs...) pack reified as a type
 Cdedekind::optimization::Polytope2DPredicate< T, Hs >:expressions predicate for the meet of N 2D halfspaces: a polytope as a single conjunctive predicate, with the halfspace pack carried at the type level so downstream combinators (argmax , and anything else dispatching on the polytope's structure) can extract it
 Cdedekind::order::Position< V >A position on the chain: just below at, or just above it
 Cdedekind::sets::PositiveInfinity
 Cdedekind::category::Pow2< N >\(k \mapsto 2^k\) on the counts, refused past the word: the window of the bit words
 Cdedekind::category::Power< C, F, N >The tensor power \(\Sigma^n\): the words of length n over the letters of a chain that a predicate keeps, a box of n legs, each the filtered alphabet, never built
 Cjlt::Power< C, F, N >The tensor power \(\Sigma^n\): the words of length n over the letters of a chain that a predicate keeps, a box of n legs, each the filtered alphabet, never built
 Cdedekind::category::PowerFunctorThe list functor on the letter maps, a word for a letter, of every length, and power(tau) for an arrow tau: the power functor \((-)^n\) at each length at once. It has no state, so it is one functor, and rev and rotate(d) are natural transformations of it to itself, by the certificates above
 Cdedekind::category::PowerMap< T >An arrow on the letters applied to every letter of a word, of any length: the list functor's action on arrows, \(\tau^{\times n}\) at each length \(n\) at once, beside power on the alphabet, Listing 4's power one level up. It commutes with every permutation of the positions, which is naturality read on words
 Cjlt::PowerMap< T >An arrow on the letters applied to every letter of a word, of any length: the list functor's action on arrows, \(\tau^{\times n}\) at each length \(n\) at once, beside power on the alphabet, Listing 4's power one level up. It commutes with every permutation of the positions, which is naturality read on words
 Cdedekind::category::Powers< C, F, N >words(Σ), the tensor powers by length, \(n \mapsto \Sigma^n\): an arrow out of the counts into the tensors, the free monoid graded by length. Its density is 1 at every length. Each power is the exponential \(\Sigma^{[n]}\), the functions from the chain of n to the letters (IsExponential, :cartesian), and the family is a strong monoidal functor \((\mathbb{N}, +) \to (\text{tensors}, \otimes)\), \(\Sigma^{m+n} \cong \Sigma^m \otimes \Sigma^n\): the box law is its monoidality (no monoidal-functor concept states it yet, #1134)
 Cdedekind::sets::Pred< K >A relational predicate built at run time: comparisons of terms and their connectives; defined after the binding below
 Cdedekind::category::Predecessor< N >The predecessor \(P : N \to N\) as an arrow, in the carrier's own posture at ⊥: the monus on ℕ (0 a fixpoint), −1 on ℤ
 Cdedekind::category::predicate_logic< P >The logic species a predicate answers in: its own, when it names one (IsSpeciesTaggedArrow), else the species of its answer type, and a composite the species of its last arrow. No type where none applies (a substitution failure, not an error). The lattice nodes over arrows and the combinators and Subobject (:topoi) read this, so a Chain<int> set (answer int, species Chain<int>) conjoins in Chain<int>, and a set pulled back along an arrow (a cylinder, χ ∘ π) answers in the set's species
 Cdedekind::category::predicate_logic< Compose< F, G > >
 Cdedekind::category::predicate_logic< P >
 Cdedekind::category::Prefixprefix("GA"): the words beginning with these letters, the predicate a section is met with. At most eight, the longest word a plan's menu holds
 Cdedekind::category::Prefixed< P, S, T >A section met with a prefix. Its own type, so that only what knows the prefix reads it: count_factors reads cycle types alone, and would count the section as if no letter were fixed, so no count is offered until it has a law
 Cdedekind::relational::Preimage< F, L >\(f^{-1} : \mathrm{Sub}(B, L) \to \mathrm{Sub}(A, L)\), substitution along \(f\): \(b \mapsto \{x \mid f(x) \in b\}\) (preimage, \(\chi_b \circ f\)). Total, a lattice homomorphism, monotone; the right adjoint of Image and the left adjoint of Dual
 Cdedekind::relational::PreimagePredicate< F, S >The preimage predicate \(a \mapsto f(a)\in S\): the subobject S pulled back along the functional arrow f ( \(\chi_S\circ f\))
 Cdedekind::category::Prior< N >The destructor \(\langle \text{is}\;Z?,\, P\rangle : N \to 1 + N\): nothing at zero, else the predecessor
 Cdedekind::category::product_algebra_base< Q >product_algebra_base<Q>: carrier-side declaration that Q is a finite direct product of some base algebra (the P operation in Birkhoff HSP). Specialise the ::type member at the carrier-defining partition (e.g.\ Vec2V<T> in linear_algebra:vec2 records product_algebra_base<Vec2V<T>>::type = T)
 Cdedekind::category::product_algebra_base< dedekind::linear_algebra::Covec2V< T > >
 Cdedekind::category::product_algebra_base< dedekind::linear_algebra::Vec2V< T > >
 Cdedekind::sets::product_cardinality< CA, CB >
 Cdedekind::sets::product_cardinality< ℵ< M >, ℵ< N > >
 Cdedekind::sets::product_cardinality< ℵ< N >, Finite >
 Cdedekind::sets::product_cardinality< Finite, ℵ< N > >
 Cdedekind::sets::product_cardinality< Finite, Finite >
 Cdedekind::category::ProductLeq< LeqA, LeqB >Componentwise product order on std::pair ≤×: (a,c)≤(b,d) :⟺ a≤b ∧ c≤d. The order-theoretic product of two posets, not the lexicographic std::less_equal on the pair
 Cdedekind::order::ProductRestrict< P, RP >The product's own membership conjoined with a relational restriction, so a bind over a restricted product keeps that membership and cannot admit pairs outside it (a full product contributes a trivially-true product)
 Cdedekind::category::Profile< E, N >The laws an arrow is known to have, one answer in K₃ per law: True where certified, Unknown where not, never False (a profile certifies, it does not refute). The pointwise lift Ω^E of the truth chain to the laws (lattice__Omega_First_Pointwise_Lift), restricted to its sub-chain Σ = {Unknown < True}: combined law by law with Inf / Sup. Read by the laws of functions below and by the laws of relations (relational:dyadic)
 Cdedekind::category::detail_comprehension::Progression< N >The progression \(j \mapsto m j + r\), a residue class's members in order: a congruence filter on a chain read as a chain of its own
 Cdedekind::relational::detail_rows::Project< K >
 Cdedekind::relational::detail_rows::Projected< K >The step of the fold building a projection: the next kept column's sort, and its equation π_{n + j} == π_c
 Cdedekind::category::Projection< K >The projection π_k: the k-th component of a product
 Cdedekind::sets::Projection< K >The projection π_k: the k-th component of a product
 Cdedekind::category::Projection< 0 >The projection out of the one-fold product A¹ ≅ A: the identity arrow (Identity), read at the point's own type
 Cdedekind::category::detail_limit::projection_arrow< K, P >
 Cdedekind::category::detail_limit::projection_arrow< 0, P >
 Cdedekind::category::detail_limit::ProjectionAt< K, P >
 Cdedekind::category::PullbackApex< Apex, A, B >The pullback apex of a meet of A and B: the apex itself, viewed with the subobject surface and the projection legs π_1 / π_2 (IsPullback)
 Cdedekind::category::detail_runs::PullsBack< N, K >The pullback's law at one count: the closed form reads what the composite P∘f reads, preimage(f, P)(x) = P(f(x))
 Cdedekind::category::PushoutApex< Apex, A, B >The pushout apex of a join of A and B: the apex viewed with the subobject surface and the coprojections ι1 / ι2 (IsPushout). Dual of PullbackApex
 Cdedekind::linear_algebra::detail_transfer::QuadDiagRule
 Cdedekind::numbers::QuadraticReal< D, Q >A real of \(\mathbb{Q}(\sqrt D)\): \(a+b\sqrt D\)
 Cdedekind::numbers::Quaternion< R >Hamilton's hypercomplex numbers q = a + bi + cj + dk
 Cdedekind::category::quotient_algebra_base< Q >quotient_algebra_base<Q>: carrier-side declaration that Q is a quotient of some base algebra. Specialise the ::type member at the carrier-defining partition (e.g.\ Complex<R> in numbers:complex records quotient_algebra_base<Complex<R>>::type = R)
 Cdedekind::category::quotient_algebra_base< dedekind::analysis::Dual< F > >
 Cdedekind::category::quotient_algebra_base< dedekind::numbers::Complex< R > >
 Cdedekind::category::quotient_congruence< Q >quotient_congruence<Q>: carrier-side declaration of the congruence witnessing Q = V/R. ::type is the relation R, ::carrier is the carrier V that R lives on (R is a homogeneous relation on V). Mirrors the S-leg's subalgebra_base
 Cdedekind::category::quotient_congruence< dedekind::morphologies::Modular< N > >
 Cdedekind::category::quotient_congruence< detail_quotient::IntByEquality >
 Cdedekind::category::detail_automaton::RandomLawsWhat the seeds say: whether the laws hold on their words, and how many sites of the subset those held, so a vacuous run can be refused
 Cdedekind::category::RandomLetterA random letter by position: the hash, read as a rank in an alphabet
 Cdedekind::relational::detail_rows::Ranges< K >A slot map by three ranges: the domain's columns, the codomain's, and the slots past the arity (a factor's own bound slots)
 Cdedekind::category::RankedA byte's rank in an alphabet: how many of its letters lie below it, the order isomorphism of the letters, in the bytes' order, onto \([0, |\Sigma|)\); a byte outside it is a hole. A Kleisli arrow into Maybe, as where is: a text of bytes read through it is the alphabet's letters, holes where it has none
 Cdedekind::numbers::Rational< Z >The Field of Fractions over an Integral Domain Z
 Cdedekind::category::detail_comprehension::Read< T, K >The coalgebra reading a bounded list position by position, each element present: a value on the stack walked as any query, so every stage composes after it
 Cdedekind::sets::ReadAs< C >The coordinate slot of the point p, read in the sort C the dispatch chose; the point itself for the unary π
 Cdedekind::category::detail_automaton::ReadBack< Section, Decoder >A code tested by a section: read back as its word, then the section's own membership
 Cdedekind::sets::Rec< S, Body >The recursion, closed: the base's membership, then the body evaluated with this very predicate in scope for its Self nodes
 Cdedekind::category::Reduce< Less, Ord, Combine >
 Cdedekind::linear_algebra::Reflected< F >Reflect an arrow through the origin of its domain: \((U f)(x) = f(-x)\) — the parity operator U precomposed onto f. The third intensional combinator (beside Scaled / PointwiseSum) that completes the surface: with them it ASSEMBLES the even projector \(P = \tfrac12(I+U)\) as scaled(½, pointwise_sum(f, reflected(f))), rather than hand-rolling pointwise + and scalar ·. Requires the domain to carry unary negation (found by ADL on the domain type)
 Cdedekind::category::detail_periodic::ReflectedAtOne byte's image under the reflection: the letter at the reflected rank, the byte itself off the alphabet. (#1141: the chain's enumeration, once alphabets range over other carriers.)
 Cdedekind::category::ReflectedReverse~rev: the reversal, then the reflection of the alphabet on every letter, the reverse complement. ~f is :posetal's: f then the reflection of its codomain's chain, which on the ranks of ACGT is \(x \mapsto 3 - x\), bitwise NOT on two bits. A word carries no alphabet, so ~rev is a family indexed by the alphabet, with a component at each, power(refl(Σ)) >> rev at Σ, taken where fixed_by(~rev) meets a power over Σ, as the exhibit's oligos & len(6) & fixed_by(~rev). Each component is an involution, two commuting involutions (commutes and is_involutive above). (#1141: an alphabet over another carrier has its component from its rank, as refl does.)
 Cjlt::ReflectedReverse~rev: the reversal, then the reflection of the alphabet on every letter, the reverse complement. ~f is :posetal's: f then the reflection of its codomain's chain, which on the ranks of ACGT is \(x \mapsto 3 - x\), bitwise NOT on two bits. A word carries no alphabet, so ~rev is a family indexed by the alphabet, with a component at each, power(refl(Σ)) >> rev at Σ, taken where fixed_by(~rev) meets a power over Σ, as the exhibit's oligos & len(6) & fixed_by(~rev). Each component is an involution, two commuting involutions (commutes and is_involutive above). (#1141: an alphabet over another carrier has its component from its rank, as refl does.)
 Cdedekind::category::Reflection
 Cjlt::Reflection
 Cdedekind::sets::rel_key< R >A comparison's key: the standard functor it is
 Cdedekind::sets::rel_key< Rel::Eq >
 Cdedekind::sets::rel_key< Rel::Ge >
 Cdedekind::sets::rel_key< Rel::Gt >
 Cdedekind::sets::rel_key< Rel::Le >
 Cdedekind::sets::rel_key< Rel::Lt >
 Cdedekind::sets::rel_key< Rel::Ne >
 Cdedekind::order::RelabelSteps< A, F, L2 >A source with every value relabelled into the species L2: a complement, a lift into a wider species, an α-cut
 Cdedekind::category::RelAnd< A, B >Meet (conjunction) of two relational predicates, the result of && on them
 Cdedekind::relational::RelAnd< A, B >Meet (conjunction) of two relational predicates, the result of && on them
 Cdedekind::sets::RelAnd< A, B >Meet (conjunction) of two relational predicates, the result of && on them
 Cdedekind::optimization::Relax< S, Cap, CostFn >Fold step of the single-source semiring closure: relax the potential at e.head through the edge e, d(v) ← d(v) ⊕ d(u) ⊗ c(u,v)
 Cdedekind::relational::RelExpr< K, Cs >A relation \(A \rightsquigarrow B\) built at run time: a term over relations, its objects dom and cod data, its classifier a reading
 Cdedekind::category::RelOr< A, B >Join (disjunction) of two relational predicates, the result of || on them, dual to RelAnd
 Cdedekind::relational::RelOr< A, B >Join (disjunction) of two relational predicates, the result of || on them, dual to RelAnd
 Cdedekind::sets::RelOr< A, B >Join (disjunction) of two relational predicates, the result of || on them, dual to RelAnd
 Cdedekind::ieee::ReportErrorPolicy< F >Report policy: keep value and attach an error envelope
 Cdedekind::analysis::ReproducingKernel< DomainSet, T >
 Cdedekind::category::detail_automaton::Residual< N, P, K >A state: whether a word of the set has just been read, and the pending words by length, pending[k - 1] those of length k
 Cdedekind::category::detail_periodic::Residue< T, N >One residue's count on a leg, appended to its histogram
 Cdedekind::sets::ResidueClass< L >The class \(\{x \in \mathbb{N} \mid x \equiv r \pmod n\}\), read analytically: the materialisation of ℕ | (π % n == r)
 Cdedekind::relational::detail_hyperdoctrine_witness::Restrict< K, UA, UB >\(\iota_K^{-1}\) as an arrow: the restriction, lifted into the sum's logic (a summand given in a smaller logic sits in the sum's by \(\Sigma \hookrightarrow \Omega\)). The right adjoint of Inject. Defined on every presentation restriction reaches: the sums, their lattice nodes, the boundaries
 Cdedekind::sets::Restrict< K, UA, UB >\(\iota_K^{-1}\) as an arrow: the restriction, lifted into the sum's logic (a summand given in a smaller logic sits in the sum's by \(\Sigma \hookrightarrow \Omega\)). The right adjoint of Inject. Defined on every presentation restriction reaches: the sums, their lattice nodes, the boundaries
 Cdedekind::category::detail_periodic::ReturnsAfter< T, N >Whether tau taken steps times returns the letter
 Cdedekind::category::detail_periodic::ReturnsTwice< T >Whether an arrow on the bytes, taken twice, returns one more byte
 Cdedekind::category::detail_periodic::ReversalAgreesThe reversal on indices agrees with position at i
 Cdedekind::category::ReverseAn involution on a carrier that is not a number: reversing a word twice is the identity, on any word a value holds, a std::string or a std::vector of letters; not a view, whose copy would alias the caller's letters. A pure function object, value in and value out, so that it is an arrow in the sense of the Jlt paper's Rule 1, and a family of them, one per word type, as std::logical_not is one per truth type; endo<W>(rev) names the domain
 Cjlt::ReverseAn involution on a carrier that is not a number: reversing a word twice is the identity, on any word a value holds, a std::string or a std::vector of letters; not a view, whose copy would alias the caller's letters. A pure function object, value in and value out, so that it is an arrow in the sense of the Jlt paper's Rule 1, and a family of them, one per word type, as std::logical_not is one per truth type; endo<W>(rev) names the domain
 Cdedekind::category::detail_involution::Reversed< Op >Op with its arguments exchanged, \(a \cdot^{op} b = b \cdot a\)
 Cdedekind::order::detail_runs::Rfl< L >
 CRigRegistration< T, Zero, One, Add, Mult >Base class for SpeciesTraits<T> of carriers forming a \emph{rig} (semiring) under (Add, Mult) with identities Zero (additive) and One (multiplicative)
 CRigRegistration< T, Zero, One, std::plus< T >, std::multiplies< T > >
 Cdedekind::category::Rolling< F, Step, Acc >A window over a periodic predicate, SQL's window function over ROWS BETWEEN CURRENT ROW AND w - 1 FOLLOWING: \(k \mapsto\) the step folded over \(f(k), \ldots, f(k + w - 1)\). A finite combination of translations, so periodic with the same period
 Cdedekind::category::detail_periodic::RotateByLetterA family of rotations that depends on the letter: each component commutes with every map on the letters, yet a map that changes the letter meets different rotations at the two ends of the square, so it is no natural transformation, and is refused
 Cdedekind::category::Rotation< N >The rotation of the positions of a word by shift, \(i \mapsto i + d \bmod n\), the symmetry of a power \(u^j\): on a word, the letter at i moves to i + d, as std::rotl moves a bit. A family of arrows, one per word type, as Reverse is
 Cjlt::Rotation< N >The rotation of the positions of a word by shift, \(i \mapsto i + d \bmod n\), the symmetry of a power \(u^j\): on a word, the letter at i moves to i + d, as std::rotl moves a bit. A family of arrows, one per word type, as Reverse is
 Cdedekind::sets::Row< Cs >A row: a point of an n-ary product whose arity and columns' sorts are data. Each cell is a value of one of the carriers Cs, and the cell's alternative is its column's sort, so a row is its own schema. Slots are π_1 … π_n
 Cdedekind::linear_algebra::RowOrientationTag for row-oriented 1-tensors (covectors, linear functionals)
 Cdedekind::category::Rule< A, B >A type-erased Morphism A -> B between Species
 Cdedekind::linear_algebra::detail_diag::rule_one_two
 Cdedekind::order::Run< C >A maximal run of membership as its closed ends, [lo, hi]
 Cdedekind::sequences::detail_pst_witness::Run< C >A maximal run of membership as its closed ends, [lo, hi]
 Cdedekind::category::RunCombineThe run lists' domain meet and join, the reducer's leaf-combine: where two leaves are run lists on one chain, the sweep, its bound the sum of theirs
 Cdedekind::category::RunList< N, K >A subset of the counts held as its steps: the positions where membership flips, strictly increasing, from outside at 0. At most K steps, so at most K / 2 runs
 Cdedekind::order::RunListSteps< N, K >Pst's run list (category:runs) as a step source: each of its steps the position just below it, the value from there on alternating from outside. Where both apply, on a finite chain with Boolean values, the order's run lists read it as any source, so ext, the merges and the cuts take it; the vocabulary they share is to move into category (#1138)
 Cdedekind::morphologies::safe_float< F >Finite IEEE-754 subset: the finiteness invariant makes the order total, so (unlike raw F) this carrier reflexively compares
 Cdedekind::category::SafeAddTransform< T >Addition with overflow check (Classical Logic)
 Cdedekind::category::detail_equality::SameIntA carrier's own equality, certified once: the laws follow
 Cdedekind::order::detail_runs::SameValueTwo steps with one value; the first step of a chunk; a step at a given value: the parts of dropping repeats
 Cdedekind::linear_algebra::Scaled< F, Mult >The scalar ⊗-action on an arrow f : D → S: \((c \odot f)(x) = c \otimes f(x)\). An IsArrow (the scaled vector), carrying the scalar c and the arrow f
 Cdedekind::sequences::ScanSteps< S >The normal form of s on the window [lo, hi], by exhaustion: a step source that walks the window (and the element after it) along chain_view and steps where χ changes, ⊥ outside the window. Lazy: one walk per traversal, nothing stored
 Cdedekind::sets::Verdict< P, K >::Search
 Cdedekind::category::Section< T, Op >A binary operation curried, with named arrows throughout (the Jlt paper, Listing 3): curry<T>(op) is \(T \to T^T\), its value at a the operator section \(b \mapsto op(a, b)\), Haskell's (a +), and uncurry takes it back to \(T \times T \to U\). A chain's end and step are such sections: curry<N>(greater_equal<N>{})(unit) stops at the unit, curry<N>(plus<N>{})(1) is the successor
 Cdedekind::category::Sections< T, Op >
 Cdedekind::sets::Self< Terms >The set under definition pulled back along the terms: χ(t₁, …) is \(x \mapsto \chi(t_1(x), \ldots)\) with \(\chi\) the comprehension's own classifier, unknown until the former closes it. A relational predicate (an operand of && / ||), evaluable only through an Env
 Cdedekind::category::SemidecidedThe verdict of a bounded search, read in K₃ along the dominance \(\Sigma \hookrightarrow \Omega\): a witness found is ⊤, none found so far is U, and nothing is ever ⊥, since the absence of a witness within a budget refutes nothing. The one arrow by which "undecided" enters a computation
 Cdedekind::linear_algebra::SemimoduleVec< S, N, Orientation >An N-entry semimodule vector over the semiring S, read as an index→scalar arrow. IsColumnVector / IsCovector by the default (semimodule) contract: ⊕ and the two-sided scalar ⊗ action, but no negation (a dioid has none). Ket (ColumnOrientation, |v⟩) and Bra (RowOrientation, ⟨w|) are its two orientations — the bra·ket language of :transfer made first-class carriers, the "matrix column/row @b is a vector" slogan for a semiring. One carrier, orientation as a template parameter (the tag is the only difference between a column and a row)
 Cdedekind::algebra::semiring_ops< S >Canonical semiring operations of a carrier, so combinators can default their Add / Mult without a call site spelling them. The default (this primary) is the ordinary ring (+, ×), which is correct for any carrier whose native operators are its semiring ops; carriers whose ops differ specialize (the burden of proof sits at the implementation site): Tropical → (⊕ = TropicalPlus, ⊗ = +), bool → (∨, ∧) — bool must NOT take the default (bool

  • bool promotes to int). This single defaulted seam replaces the old detection(empty-primary)/resolution(semiring_ops_of) split
 Cdedekind::algebra::semiring_ops< bool >The Boolean semiring's operations, (∨, ∧)
 Cdedekind::algebra::semiring_ops< dedekind::linear_algebra::MatNxNV< S, N > >Mat(S) is a semiring: register its ⊕ / ⊗ so downstream (e.g. :transfer's star = the *-closure) reads them generically off semiring_ops, exactly as for the base S
 Cdedekind::algebra::semiring_ops< Tropical< T, M > >The tropical semiring's operations, (⊕ = TropicalPlus, ⊗ = +): its own, not the ring's, registered on :universal's semiring_ops
 Cdedekind::sequences::SequenceGraph< PathT >as_relation(path) — adapt a Path<T> into its graph relation, a Set of (index, value) pairs
 Cdedekind::category::Set< T >The Category of C++ Types (Set). Formally reified as a Cartesian Closed Category
 Cdedekind::sets::set_predicate< S >The predicate of a PLAIN set, a Comprehension over the universe 𝔸<T,L> (::type absent otherwise); PlainSet gates the plain-set-only branches (complement pair, predicate negation) so a compound node (Meet / Join) takes the node path
 Cdedekind::sets::set_predicate< Comprehension< 𝔸< T, L, C >, P > >
 Cdedekind::category::detail_periodic::SetBit< W >One letter's bit into the packed characteristic function
 Cdedekind::category::detail_periodic::SetByteOne letter into a packed set of bytes
 Cdedekind::sets::SetCombineThe injected leaf-combiner (the reducer's Combine policy) for the subobject lattice: at an order-incomparable residual, hand the two set leaves to the carrier's domain ∧ / ∨ on their runtime data and let the reducer fold the result again. Two plain sets over one universe combine through their predicates (structured_and / structured_or via ADL, elevated back to a set); a value leaf (an Interval) combines directly. Each leg is present only where the carrier actually combines the pair, so elsewhere the residual stays a Meet / Join node
 Cdedekind::sets::SetExpr< Derived, DomainT, L >Opt-in CRTP base that supplies the ETCS set surface to a specialized set expression. It provides Member, ι (the subobject inclusion), Codomain, logic_species, and the set-lattice trait members. It keys the classifier χ off the Derived's own operator()
 Cdedekind::sets::SetExpr< BoundedSet< OI, P >, OI::Domain, OI::logic_species >
 Cdedekind::sets::SetExpr< Comprehension< Base, Predicate >, Base::Domain, comprehension_logic_t< Base, Predicate > >
 Cdedekind::sets::SetExpr< Interval< V, Boole >, V, Boole >
 Cdedekind::sets::SetExpr< Runs< V, Boole >, V, Boole >
 Cdedekind::sets::SetExpr< Sub< C, Boole >, C, Boole >
 Cdedekind::sets::SetExpr< Sub< C, L >, C, L >
 Cdedekind::category::SetId< T >The Identity morphism for the category Set
 Cdedekind::category::detail_automaton::SetLetterOne more letter of a power, into the set of them
 Cdedekind::sets::SetObjectLeafA leaf that is a set object, the property over_nodes lifts
 Cdedekind::category::detail_etcs_total_witness::SetOverNonRegular
 Cdedekind::relational::detail_hyperdoctrine_witness::Seven
 Cdedekind::category::Shift< N >A translation of the counts, \(k \mapsto k + j\): after it, a periodic arrow keeps its period, on an extent narrowed by j
 Cdedekind::sets::ShiftDown< K >The slots above an eliminated bound slot, moved down by one
 Cdedekind::algebra::Signature< Ops >A signature, the \(F\) of an \((A, F)\) algebra named as one type: the Ops... of IsAlgebra, IsAlgebraOnSet and HasCarrier, which a concept can then take as a parameter and default
 Cdedekind::category::signature_extractor< F >
 Cdedekind::sets::SignedExtensionalCardinal< S >Signed one-word integer: two's complement in the signed word S
 Cdedekind::optimization::Singleton2DPredicate< T, x_val, y_val >:expressions predicate for the LP's unique optimal vertex at NTTP coordinates
 Cdedekind::category::Slice< C >The chain of C restricted by value to [lo, hi): the elements from lo up to hi, hi excluded, as pandas' .loc reads a slice. For any carrier with the covering step, std::byte among them
 Cdedekind::category::detail_chain::SliceStep< C, F >The step of a chain restricted by value to [lo, hi): f of the element and its cover, while the element is below hi
 Cdedekind::sets::SlotsThe slot algebra: the slots a term or a relational predicate mentions, as a bit mask (bit i for π_i, bit 0 for the unary π). A node mentions the union of its legs' slots; a predicate the grammar does not know mentions every slot, so no certificate reads more into it than it says
 Cdedekind::relational::detail_rows::SortsSoFarThe step of a ∧ over a row's cells: the next cell has the next column's sort. The fold's state is the verdict so far and the column reached
 Cdedekind::order::SourceRef< S >A source read through a reference: a stored run list inside a term is traversed where it is, not copied
 Cdedekind::order::Span< V >The sides of an inhabited convex set; an absent side is unbounded
 Cdedekind::order::SpanSteps< V, L >An interval's sides as a source, valued value on it and ⊥ elsewhere: at most two steps. No sides is the whole carrier, no span the empty set, so the constants are spans too
 Cdedekind::category::species_embed< From, To >The embedding From ↪ To of one species' answers into another's, preserving ⊥, ⊤, ∧, ∨ and ¬ (a De Morgan embedding), so that the set complement ~ commutes with every lift
 Cdedekind::category::species_embed< Boole, To >
 Cdedekind::category::species_embed< Kleene, Percent >
 Cdedekind::category::species_embed< L, L >
 Cdedekind::category::SpeciesTraits< T, Args >
 Cdedekind::category::SpeciesTraits< dedekind::algebra::Monomial< N > >
 Cdedekind::category::SpeciesTraits< dedekind::algebra::OneDimensionalVector< S, Tag > >
 Cdedekind::category::SpeciesTraits< dedekind::ieee::IEEE< F > >
 Cdedekind::category::SpeciesTraits< dedekind::morphologies::Modular< N > >
 Cdedekind::category::SpeciesTraits< dedekind::numbers::Complex< R > >
 Cdedekind::category::SpeciesTraits< dedekind::numbers::Cut< Q > >Atlas registration: Cut<Q> is a first-class species
 Cdedekind::category::SpeciesTraits< dedekind::numbers::QuadraticReal< D, Q > >Atlas registration: QuadraticReal<D,Q> is a first-class species
 Cdedekind::category::SpeciesTraits< dedekind::numbers::Rational< Z > >
 Cdedekind::category::SpeciesTraits< dedekind::sets::Cardinality >
 Cdedekind::category::SpeciesTraits< dedekind::sets::SignedCardinality >
 Cdedekind::category::SpeciesTraits< dedekind::sets::SignedExtensionalCardinal< S > >
 Cdedekind::category::SpeciesTraits< std::pair< A, B > >
 Cdedekind::category::SpeciesTraits< std::tuple< Ts... > >
 Cdedekind::category::SpeciesTraits< T >
 Cdedekind::category::SpeciesTraits< Truth< L > >Bridge the Monic Wrapper to the Logic Species Registry
 Cdedekind::category::SplitMixA random number as an arrow out of the counts, a sequence on a chain: the hash of a position and a seed (SplitMix64, Steele, Lea and Flood 2014). constexpr, with no state: any position is at hand, a sequence of any length is never stored, and two seeds are two streams. So a law can be asked of random inputs in a static_assert, and a million events cost nothing to spin up. For exercising code: no cryptography, and no claim on sampling
 Cdedekind::category::detail_runs::Along< Pred, N, K >::State
 Cdedekind::category::detail_runs::Sweep< N, J, K, Op >::State
 Cdedekind::order::detail_runs::FoldPieces< Op, L >::StateThe value of the piece being read, and the fold of the pieces before it, none before the first piece inside the carrier
 Cdedekind::linear_algebra::StaticRankNullity< AmbientDimension, Rank >Convenience compile-time carrier for finite-dimensional witnesses
 Cdedekind::order::Step< V, L >Where the value changes, and to what. A source holds its steps by value (an interval's two sides, an iterator's current step), so the carrier and the truth values are default-initialisable
 Cdedekind::category::detail_kleisli::StepAt< Step, A, X, TA >The step at one element, a Kleisli arrow \(A \to T(A)\)
 Cdedekind::category::StepCoalgebra< X, Step >The coalgebra of a partial step \(X \to 1 + X\): the element, and the step as the next state, while the step has a value. Turns Prior, lower_cover or cover into a lens
 Cdedekind::category::detail_comprehension::StepFrom< Op, R >A fold step with its accumulator bound, \(a \mapsto \mathit{op}(\mathit{acc}, a)\): the present case of the eliminator
 Cdedekind::order::detail_steps::Steps< L >The normal form of a set term as the algebra of cata: an interval's sides, a stored run list read in place, the boundaries as constants; a meet or join the merge of its legs' steps under ∧ or ∨, a complement their relabelling by ¬. Lazy: nothing is stored, the steps are pulled by the query that reads them
 Cdedekind::order::detail_cover_witness::StepTowardOne successor step of a walk that looks for b
 Cdedekind::category::StringArrowAn arrow that is just a label
 Cdedekind::category::StringCategoryThe Category of Labels
 Cdedekind::order::detail_connective::StructurallyBeforea before b in the structural order
 Cdedekind::order::detail_connective::StructurallySamea and b the same tree (equivalent in the structural order)
 Cdedekind::category::subalgebra_base< S >subalgebra_base: carrier-side declaration that S is a subalgebra of some base algebra (the S operation in Birkhoff HSP). Specialise the ::type member at the carrier-defining partition; the propagation specs below then lift the species-trait pins from base to S
 Cdedekind::category::Subobject< A, Chi >The Subobject Species S ↣ A
 Cdedekind::sets::subobject_order< L >The subset (⊆) order on the subobject lattice Sub(T), keyed by the logic species L. This is the injected order (Ord) under which the generic lattice-law term reducer (category:lattice_term, #865/#890) normalises set expressions: Ø is its bottom (⊥, initial), 𝔸 its top (⊤, terminal). Keying by L lets the algebra markers distinguish Boole (a Boolean subobject lattice, every law) from Kleene (Heyting / De Morgan, no complement collapse)
 Cdedekind::category::SubobjectClassifier< T >
 Cdedekind::category::SubobjectInclusion< S >inclusion_arrow(S): the inclusion \(\iota_S : S \hookrightarrow \mathrm{Domain}(S)\) of a subobject as an arrow (Domain = S::Member, Codomain = S::Domain, through S's own ι), so it can be a leg of a cospan. A monomorphism by definition
 Cdedekind::sets::Subobjects< T, L >The subobjects of a carrier in a logic, \(\mathrm{Sub}(T, L)\) ( \(\mathrm{Sub}(\mathbb{A}_T)\), \(\chi\) valued in L), as an object: the domain or codomain of an arrow on sets — the complement, the pushforward along an injection. No one type is this object: every set object over the carrier in that logic presents it (the expression grammar is a type-indexed family: 𝔸, a comprehension, a Meet / Join / Not node), and the universe, its top, is the representative, so category::IsArrow checks an arrow on sets at the universe and asks the result to be a set object over it (morphism__Objects_And_Their_Presentations). A universe's cardinality class is a bound, not part of the object
 Cdedekind::category::detail_comprehension::SubrangeAt< R >
 Cdedekind::order::SubsetOf< C, L >The membership predicate of 𝔓(S): \(X \mapsto X \subseteq S\), with S coerced to Sub(C). A named functor (no lambda)
 Cdedekind::sets::Term< K >::SubstOneThe one-slot substitution as a slot map
 Cdedekind::category::Successor< N >The successor \(S : N \to N\) as an arrow, over any carrier with the NNO step: the one spelling of the Peano successor where an IsArrow is needed (image, graph, the NNO witness), in place of a struct per site
 Cdedekind::morphologies::singleton_image_breadcrumb::Successor< N >The successor \(S : N \to N\) as an arrow, over any carrier with the NNO step: the one spelling of the Peano successor where an IsArrow is needed (image, graph, the NNO witness), in place of a struct per site
 Cdedekind::sets::sum_universe< UA, UB >The sum of two set objects: the subobject (a, b) of the coproduct of their carriers, \(|a + b| = |a| + |b|\) (the join on the cardinal lattice, as for the product). Reduced where the types decide it:
 Cdedekind::sets::sum_universe< 𝔸< X, LA, CA >, 𝔸< Y, LB, CB > >
 Cdedekind::sets::SumMembership< A, B >Membership of a sum: the copairing \([\chi_a, \chi_b]\), each answer lifted into the join of the summands' species. A named functor (the product's dual is the meet of its cylinders, ProductMembership)
 Cdedekind::category::SupValue-returning chain lattice ops — the honest T × T → T meet / join
 Cdedekind::category::SwapPred< P >The swapped predicate for converse: \(R^\smile(b,a) = R(a,b)\)
 Cdedekind::relational::SwapPred< P >The swapped predicate for converse: \(R^\smile(b,a) = R(a,b)\)
 Cdedekind::category::detail_runs::Sweep< N, J, K, Op >One position of a sweep: the operation's value there, kept as a step where it differs from the value before
 Cdedekind::sets::SymbolicImagePredicate< U >Symbolic image-of-intensional-Set predicate (#602 layer 1)
 Cdedekind::category::Symmetric< P, S, T >The section of a tensor power fixed by a permutation sigma of the positions and an arrow tau on the letters, \(x_{\sigma(i)} = \tau(x_i)\): the legs merged along each cycle of sigma, the spider's Merge through tau, the words de Bruijn's power group element \((\sigma, \tau)\) fixes
 Cdedekind::sequences::TailEquivalent< T >The tail-equivalence relation on Path<T>: agreement on a sampled tail window [start, start+span)
 Cdedekind::category::Take< K >take<K>(), SQL's LIMIT: the first K present elements
 Cdedekind::category::detail_comprehension::Taken< S, Coalg, K >The coalgebra of take<K>: the walk, until K elements are present. One more state, the count so far; O(1), no storage
 Cdedekind::category::detail_comprehension::Tally< N >One more element into a count
 Cdedekind::geometry::TangentBundlePoint< F, N >A point in the tangent bundle T(F^N) = F^N × F^N
 Cdedekind::category::Tensor< R, S >The parallel product ⊗ as the arrow-half of the product bifunctor: R⊗S : A×B→C×D is IsProduct acting on the morphism pair (R,S). The object-half is IsProduct itself (the carrier A×B is the product object); the arrow-half is this Tensor. The action is the mediating morphism ⟨R∘π₁, S∘π₂⟩ built from the product's own reified projections Π<1, P> / Π<2, P> (:limit) and its pairing (the std::pair mediator mediate_product wraps as an arrow); nothing here reimplements the universal property
 Cdedekind::sets::Term< K >A term built at run time, the grammar with its shape a value; defined after the binding below
 Cdedekind::category::detail::TerminalEnvelope
 Cdedekind::category::TernaryResult< T >A Logic-Aware Result container for Ternary outcomes
 Cdedekind::category::detail_periodic::TimesPower< N >One factor into the product: \(b^e\) is e copies of b under *, which concat on copies computes by squaring, Listing 4's overload at the monoid \((\mathbb{N}/2^w, \times)\); the factors are then the plain fold, one multiplication each
 Cdedekind::category::detail_periodic::ToByteA character as a byte
 Cdedekind::order::detail_runs::ToItself< C, L >An element as the step to its own value: χ = id
 Cdedekind::sequences::detail_pst::ToMembership< S >An element of the walk as the step to its membership, ⊥ past the window's top
 Cdedekind::category::detail::topo_bad_sieve_codomain_mismatch
 Cdedekind::category::detail::topo_bundle_witness
 Cdedekind::category::detail::topo_demo_arrow
 Cdedekind::category::detail::topo_demo_bool_arrow
 Cdedekind::category::detail::topo_demo_sieve
 Cdedekind::category::detail::topo_demo_topology
 Cdedekind::category::detail::topo_projection_arrow
 Cdedekind::order::detail_runs::ToStep< V, L >A breakpoint of a map as a step
 Cdedekind::sets::Total< X >The totality algebra at the points X: a node is total when its legs are, and an operator when it is admitted on its carrier (admits, the gate the value algebra enforces: total there, or dividing by a nonzero constant), an applied arrow when the arrow is total and its argument already has the arrow's domain (a conversion may fail). A predicate the grammar does not know is not certified
 Cdedekind::sequences::detail::toy_countable_family< T >
 Cdedekind::category::_kleisli_arrow_witness_380::toy_partial_realize
 Cdedekind::category::image_decidability_witness::ToyEmbed
 Cdedekind::category::image_decidability_witness::ToyGeneral
 Cdedekind::category::image_decidability_witness::ToyRetract
 Cdedekind::category::detail_runs::Translated< N, K >One step of a preimage along a translation: a step past it moves down by it; one at or before it is absorbed into the value at 0
 Cdedekind::linear_algebra::TransposeF< S, N >The transpose reified as a dagger functor: TransposeF{}(A) = Aᵀ. A value/type (not a free call), so the point-free dedekind::category dagger predicates and concepts (is_unitary, IsDagger, IsUnitary) can take it as their Dagger argument. On Mat(S) the dagger is the transpose; on Rel it is converse; on a Hilbert space the adjoint — :involution unifies the three
 Cdedekind::algebra::Tropical< T, Max >Tropical carrier T ∪ {∞}. finite==false is the ⊕-identity sentinel (−∞ for Max, +∞ for Min), absorbing under ⊗. operator+ is ⊗ (honest addition); ⊕ is TropicalPlus
 Cdedekind::algebra::TropicalPlus⊕: the tropical addition, the order-extremum (a semilattice join for Max, meet for Min). Named, not an operator, so a+b never silently means max
 Cstd::true_type
 Cdedekind::category::Truth< L >The Monic Wrapper for a Logical Species (Ω)
 Cdedekind::category::tuple_functor< T >The Intensional Functor for 1-tuple values
 Cdedekind::category::tuple_monad_tag
 Cdedekind::category::TupleMap< T, F >f on the one element of a one-tuple: the one-tuple functor's action on an arrow
 Cdedekind::analysis::TwoForm< F, N >An antisymmetric bilinear form ω(u, v) = -ω(v, u)
 Cdedekind::category::Uncurried< T, Op >\(T \times T \to U\): the curried operation, taken back
 Cdedekind::category::Unfold< S, Coalg >The anamorphism of a coalgebra as an arrow from the seeds: x >> unfold<S>(c) is unfold(x, c)
 Cdedekind::category::unit_registry< T, Op >
 Cdedekind::category::unit_registry< bool, Op >
 Cdedekind::category::unit_registry< ConstantMorphism< A, B >, Op >unit_registry specialisation for ConstantMorphism<A, B>. Registers the constant-at-identity-element-of-B as the identity element of ConstantMorphism<A, B> under operation Op
 Cdedekind::category::unit_registry< T, Op >
 Cdedekind::category::unit_registry< T, std::multiplies< T > >
 Cdedekind::category::unit_registry< T, std::plus< T > >
 Cdedekind::category::unit_witness< Functor, T >Unit_witness<Functor, T>: Generic Kleisli unit witness. Lifts a value into the Kleisli extension named by Functor::template Shape<T>
 Cdedekind::category::unit_witness< dedekind::linear_algebra::covec2_functor< T >, T >
 Cdedekind::category::unit_witness< dedekind::linear_algebra::matrix2x2_functor< T >, T >
 Cdedekind::category::unit_witness< dedekind::linear_algebra::vec2_functor< T >, T >
 Cdedekind::category::unit_witness< maybe_functor< T >, T >
 Cdedekind::category::unit_witness< path_functor< T >, T >
 Cdedekind::category::unit_witness< tuple_functor< T >, T >
 Cdedekind::numbers::UnitRoot< N >A SYMBOLIC N-th root of unity \(\zeta_N^{\,p}\), carried by its exponent p ∈ ℤ/N (Modular<N>). The unit harmonics \(\mu_N=\{z:z^N=1\}\): the torsion subgroup of the unit circle U(1), cut out of ℂ, cyclic of order N and \(\cong\mathbb{Z}/N\) via de Moivre
 Cdedekind::sets::UniversalPredicate< T >The universal predicate: accepts every element of T
 Cdedekind::sets::universe_cardinality< U >The cardinality class of a set object's universe
 Cdedekind::sets::universe_cardinality< 𝔸< T, L, C > >
 Cdedekind::sets::UnknownPredicate< T >The archetypal undecidable predicate: answers Unknown everywhere
 Cdedekind::category::detail_ordinal_sum::Unordered
 Cdedekind::category::Unpack< W >A machine word read back as the count of its pattern: the retraction of pack, \(\mathit{unpack} \circ \mathit{pack} = \mathrm{id}\) on the counts below \(2^W\). Up to a machine word, since a count is one
 Cdedekind::order::detail_halfspace_witness::UnrelatedCardinalityAlias
 Cdedekind::category::Until< End, Step >The chain in arrows (the Jlt paper, Listing 3). Three arrows make it: an end, a predicate on the states; a step, an endo; a seed, a point. until(end, step) is the guard, after the Haskell Prelude's until, the partial step \(N \to 1 + N\) a cartesian category builds as \(\langle end, 1\rangle ; dist ; (! + step)\). chain(out) is the anamorphism as an arrow \(N \to N^*\), so a seed composed into it, x >> chain(out), is its chain. ns >> f is the functor's action, f mapped over the elements, the coalgebra's emitted leg post-composed, \((1 + f \times 1) \circ out\), and map id is the chain itself, decided at the type. A fold over the composite is a hylomorphism: nothing between the seed and the fold is built
 Cdedekind::sets::Value< P >The value algebra: a term or a predicate folded at the point p. A projection reads its coordinate, a constant is its value, a predicate the grammar does not know is evaluated as itself; an operator or a comparison combines its operands in the carrier of the non-constant one; an applied arrow converts its argument into its domain
 Cdedekind::sets::value_sum< Sorts >The value of a term built at run time at a point: the one sort's carrier, or the sum of the sorts where there are more
 Cdedekind::sets::value_sum< std::tuple< A > >
 Cdedekind::sets::value_sum< std::tuple< A, B, Cs... > >
 Cdedekind::order::detail_runs::ValueIs< Ω >
 Cdedekind::linear_algebra::Vec2< T, x, y >Structural 2-tuple with coordinates at the type level
 Cdedekind::optimization::Vec2< T, x, y >Structural 2-tuple with coordinates at the type level
 Cdedekind::linear_algebra::vec2_functor< T >
 Cdedekind::linear_algebra::Vec2Map< T, F >f on every entry: the vec2_functor's action on an arrow, an endomap of the entries applied entrywise
 Cdedekind::linear_algebra::Vec2V< T >Value-level column vector of length 2, viewed as a 2×1 matrix
 Cdedekind::geometry::Vector< F, N >An element of a Coordinate Space over a Field F
 Cdedekind::sets::Verdict< P, K >
 Cdedekind::optimization::VertexCandidate< T >Reduction output: optimum coordinates with a feasibility flag
 Cdedekind::category::vertical_composition< Α, Β, F, G, H >Vertical composition of two 2-morphisms (β . α)
 Cstd::ranges::view_interface
 Cdedekind::category::detail_automaton::Walk< Sigma, N, P, K, KL, Q >One state walked, in the order found: its row of transitions, and whether it accepts. Past the states found, nothing to walk
 Cdedekind::order::detail_cover_witness::WalkA walk along the cover: where it is, and whether it met b
 Cdedekind::linear_algebra::detail_transfer::WeightedUnitPath
 Cdedekind::category::Where< P >where(p), SQL's WHERE: the Kleisli arrow into Maybe that keeps an element where p holds, a hole where it does not. The walk keeps its length, so a filtered chain is a chain in the same order
 Cdedekind::category::Window< N >The window of a word from position offset, length letters long: its projection onto those positions, \(\pi_I\) for \(I = \{\mathit{offset}, \ldots, \mathit{offset} + \mathit{length} - 1\}\), a factor of the word in the sense of combinatorics on words. Total: a window past the word's end is cut at it, so it is shorter
 Cdedekind::category::WindowJoin< P, S >p >> s, SQL's JOIN on a window: the tensor of the windows of the words of p that land in s, at every offset where a window fits. A constructor, not a materialisation: the join is a tensor, counted, never enumerated, so it stays inside the counted world and never meets the bag a join yielding rows would need
 Cdedekind::category::Windowswindows(n), the stage that reads each position's window of n elements, a position with its context, as a comonad's \(\delta\) would on an infinite stream; on a finite range the last n - 1 positions have no full window, so it is not a comonad here. It is std::views::slide(n), spelled as a stage
 Cdedekind::category::detail_periodic::WindowStep< F, Step >One step of a window at k: the step applied to f(k + j)
 Cdedekind::category::detail_periodic::WithOne more value into a bounded list, as a fold's step
 Cdedekind::sets::with_carrier< S, C >The tuple S with C appended, unless C is in it already
 Cdedekind::sets::with_carrier< std::tuple< Cs... >, C >
 Cdedekind::category::detail_automaton::WithLetters< Sigma, Q >A plan with the columns of its alphabet's bytes
 Cdedekind::relational::detail_rows::WithSlotThe step of the fold for column_mask: one slot's bit more
 Cdedekind::linear_algebra::zero_rule< T >Zero rule: i ↦ T{0}
 Cdedekind::category::ZeroAction< A, B, Op >The 'Absorption' logic
 Cdedekind::category::ZeroElement< N >The zero element \(Z : 1 \to N\), the nullary IsNNO witness: the carrier's default value, which is the NNO's zero for the integrals and for Cardinality. Nullary, so not an IsArrow (that concept asks for a Domain); a composable \(1 \to N\) arrow is not needed here
 CZ