dedekind.category Module Reference

Concepts
concept	dedekind::category::IsNNO
	Structural shape: (N, Z, S) is a Natural Numbers Object — Z is the zero element 1 → N, S is the successor map N → N.
concept	dedekind::category::HasNNOStep
	A carrier with both NNO steps available: the shape a value-determined point collapse needs (succ(lo) == pred(hi)).
concept	dedekind::category::IsFunctor
	The textbook functor (#633): an IsArrow whose Domain and Codomain are (small) categories — a 1-morphism in Cat, Mac Lane §I.3 — carrying a morphism map.
concept	dedekind::category::IsShapedFunctor
	A 1-morphism mapping CatS -> CatT, refined with the container shape: an IsFunctor that additionally exposes a type-level object map Shape and the action on arrows, F(f).
concept	dedekind::category::IsIdentityFunctor
concept	dedekind::category::IsEndofunctor
	A structure-preserving mapping from a Category back to itself (F : 𝒞 → 𝒞).
concept	dedekind::category::IsIterativeEndomorphism
	A stabilizing step function on a carrier species.
concept	dedekind::category::IsFAlgebra
	A carrier A equipped with a structure map F<A> -> A.
concept	dedekind::category::IsFCoalgebra
	A carrier A equipped with a structure map A -> F<A>.
concept	dedekind::category::IsEmbeddingFunctor
	A functor that is fully faithful + injective on objects (Mac Lane CWM §IV.4 strong reading; the Yoneda-embedding flavour).
concept	dedekind::category::IsQuotientFunctor
	A functor that is a regular epi / coequalizer presentation (Borceux Handbook §4.3).
concept	dedekind::category::IsPeriodic
	Taxonomic Decorator: Certifies that an operation is circular (wraps). This is the "Safety Certificate" for machine totality.
concept	dedekind::category::IsSaturating
	Taxonomic Decorator: certifies that an operation reaches out-of-range values via a saturating escalation (e.g.\ \(\pm \aleph_0\)) rather than wrapping or being undefined.
concept	dedekind::category::IsClosedUnder
	(S, Op) is closed under a binary operation: Op{}(s_1, s_2) returns a value of type S for any S-typed operands. The textbook closure axiom expressed structurally — no opt-in trait needed because closure is deducible from the operator's signature.
concept	dedekind::category::IsClosedUnderUnary
	Unary closure variant: Op{}(s) returns S for any S-typed operand. Cardinality has no IsClosedUnderUnary for std::negate<> (negation of a positive natural would need to land outside ℕ); that's the structural witness that -Cardinality is closure-forcing rather than closed.
concept	dedekind::category::IsClosedUnderEither
	(T, Op) is closed under Op, where Op may be either binary or unary. Distinct from IsClosedUnder (binary) so call sites that need a specific arity stay typo-proof.
concept	dedekind::category::IsConstructed
	D declares a construction: a base and the shape of its ×.
concept	dedekind::category::IsTotal
	The Master Safety Certificate for Level 0: is_total, as a concept.
concept	dedekind::category::IsTotalArrow
	A Morphism whose domain species admits no undefined (hazard) values.
concept	dedekind::category::IsPointed
	A type T has a chosen identity element under operation Op.
concept	dedekind::category::IsMagma
	T × T → T (The Base Total Species).
concept	dedekind::category::IsUnitalMagma
	A Magma with a global Identity (0 or 1).
concept	dedekind::category::IsInvertible
	A pointed (T, Op) where every element has an Op-inverse.
concept	dedekind::category::IsLoop
	A UnitalMagma with Inverses (-x).
concept	dedekind::category::IsSemigroup
	An Associative Magma.
concept	dedekind::category::IsCommutativeSemigroup
	An Associative Magma where the operation is also commutative.
concept	dedekind::category::IsMonoid
	A Semigroup with a two-sided Identity element.
concept	dedekind::category::IsMonoidHomomorphism
	A map between two monoids, (T, Op) and its image under Op2, that carries the operation, declared on every pair, and the unit to the unit, computed (:morphism's PreservesUnit).
concept	dedekind::category::IsCommutativeMonoid
	A Monoid where the operation is commutative.
concept	dedekind::category::IsGroup
	A Monoid with two-sided Inverses (The Perfect Symmetry).
concept	dedekind::category::IsAbelianGroup
	A Commutative Group.
concept	dedekind::category::IsCyclicGroup
	A cyclic abelian group: the honest concept name for \(\mathbb{Z}/n\mathbb{Z}\) carriers and their machine-backed cousins.
concept	dedekind::category::IsRig
	A Semiring without Negatives (Addition is a Monoid).
concept	dedekind::category::IsRng
	A Ring without Identity (Multiplication is a Semigroup).
concept	dedekind::category::IsSemiring
	Alias for IsRig: a general multi-operation species.
concept	dedekind::category::IsRing
	The Perfect Species (Rig ∩ Rng).
concept	dedekind::category::IsCommutativeRing
	A Ring whose multiplication is commutative.
concept	dedekind::category::IsField
	The axiomatic field witness — a commutative ring whose multiplicative structure is an abelian group (zero excluded, by convention on is_invertible_v).
concept	dedekind::category::IsJoinSemilattice
	A Semilattice used as the "join" (least upper bound / ∨) half of a Lattice. In bool this is logical_or; in int it is max.
concept	dedekind::category::IsMeetSemilattice
	A Semilattice used as the "meet" (greatest lower bound / ∧) half of a Lattice. In bool this is logical_and; in int it is min.
concept	dedekind::category::IsLattice
	compatibility alias for order-lattice refinement.
concept	dedekind::category::IsDistributiveLattice
	compatibility alias for distributive order lattices.
concept	dedekind::category::IsBoundedLattice
	A IsLattice whose join and meet each carry an identity: the bottom \(\bot\) (unit<T>(Join{})) and top \(\top\) (unit<T>(Meet{})).
concept	dedekind::category::IsBooleanAlgebra
	The top of the Boolean-algebra variety Alg(∨,∧,¬,⊥,⊤): a complemented distributive bounded lattice — the ∨/∧/¬ analogue of IsField topping the (signature-expanded) ring variety.
concept	dedekind::category::HasClosureForcingShape
	Structural shape: Op{} sends (A, A) → B (binary) or A → B (unary) with A ≠ B. Pure deducible clause of IsClosureForcing. The universal-property side — that B is the smallest carrier closing Op over A — is carried by the is_closure_forcing_v opt-in trait below.
concept	dedekind::category::IsClosureForcing
	Composite: structural shape + opt-in canonicality. The full witness that Op is the closure-forcing operator A → B (or A × A → B), with B the canonical recipient.
concept	dedekind::category::IsCopies
	A range of n copies of one value, Bird's replicate n x, whose fold under a monoid is the power \(x^n\); n and the value known without walking it: copies_count(r) and copies_value(r), which each model supplies, declared above so that ordinary lookup finds them for models outside this namespace, the standard's among them.
concept	dedekind::category::IsMorphicTotal
	A Morphism whose Codomain is the Terminal Object (One).
concept	dedekind::category::IsTerminalMorphism
	A morphism that maps into the Terminal Object (One).
concept	dedekind::category::IsTerminalObject
	A type that plays the role of a terminal object — either the canonical global One (std::monostate, the unique terminal of the ambient category of sets) or an opt-in structural witness via the is_terminal_object_tag typedef.
concept	dedekind::category::IsBoundaryProjection
	Projection witness from an owning/wrapper whole to a boundary object.
concept	dedekind::category::IsProjectedTerminalObject
	Terminal-object witness through an optional projection policy.
concept	dedekind::category::HasUniqueMorphismTo
	Asserts that there exists a unique morphism from T to U = One.
concept	dedekind::category::HasUniqueMorphismFrom
	Asserts that there exists a unique (unreachable) morphism from Z = Zero to T.
concept	dedekind::category::IsInitialObject
	A type that plays the role of an initial object — either the canonical global Zero (std::nullptr_t, the unique initial of the ambient category of sets) or an opt-in structural witness via the is_initial_object_tag typedef.
concept	dedekind::category::IsBoundaryObject
	A type at a lattice / category bound: an initial object (⊥) or a terminal object (⊤).
concept	dedekind::category::IsProjectedInitialObject
	Initial-object witness through an optional projection policy.
concept	dedekind::category::IsPairProjection
	Whether F is the projection \(\pi_K\) out of a pair: the recogniser the law readers (:cartesian, a product's defining form) and the hyperdoctrine (relational:graph) read. A genuine std::pair only: a pair-like carrier with more state is no product of its two members.
concept	dedekind::category::IsProduct
	Categorification of std::pair<A, B> as the categorical product (A × B).
concept	dedekind::category::IsArrowProduct
	An IsProduct whose projections are genuine MORPHISMS (arrows), not merely the structural callables IsProduct checks.
concept	dedekind::category::IsProductProjection
	Functional-part projection witness from a product whole to one part.
concept	dedekind::category::IsProjectedProduct
	Product witness through an optional whole-projection policy.
concept	dedekind::category::IsArrowFromProduct
	Matches an Arrow whose Domain is a categorical Product (std::pair).
concept	dedekind::category::IsProductParthood
	Bridge: a product P with parts A and B IS a mereological parthood in the projection-access reading.
concept	dedekind::category::IsCartesian
	A small category equipped with a terminal object 1 and binary products × — a "cartesian category" in the textbook sense (Pierce, Basic Category Theory for Computer Scientists §1.4; Awodey).
concept	dedekind::category::SetAsProduct
	Set := (Underlying, Classifier) read as a product, in the projection-access sense.
concept	dedekind::category::IsConcrete
	A small category C is concrete when its objects are themselves sets — equivalently, when there is a faithful functor U : C → Set.
concept	dedekind::category::HasTernarySupport
	True when a set object's classifier returns ternary truth values.
concept	dedekind::category::IsCompatibleSetPair
	Two set objects over the same ambient species and same Ω codomain.
concept	dedekind::category::HasPeriod
	A sequence on finite chains with a declared period, read by period(f): \(f(k + p) = f(k)\) for every k. Periodicity is a sequence's, an arrow out of the counts, not an arrow's in general.
concept	dedekind::category::HasUnitPeriod
	A sequence constant on its extent by its type: a constant arrow out of the counts, a sequence after one, and the cylinder's factors along the offsets (R2).
concept	dedekind::category::HasCycleType
	A permutation of positions with a known cycle type.
concept	dedekind::category::HasFactors
	A tensor whose count is a product of factors, as many as its type bounds: a shape, so an outer product of two is one too.
concept	dedekind::category::IsDirected
	Formal verification of the directedness axiom: ∀ a, b ∈ T. ∃ c ∈ T. Rel(a, c) ∧ Rel(b, c).
concept	dedekind::category::IsCodirected
	Formal verification of the codirectedness axiom: ∀ a, b ∈ T. ∃ c ∈ T. Rel(c, a) ∧ Rel(c, b).
concept	dedekind::category::IsFilteredCategory
	A thin category whose every finite subset of objects has an upper bound (directedness).
concept	dedekind::category::IsLatticeLess
	The injected total order: a caller-supplied comparator with a static consteval less<X,Y>() returning a logic value in its lattice_less_logic (default Boole, i.e. bool). The reported logic must be a full IsOckhamAlgebra, so ::True (accessed by lattice_definitely_less) is guaranteed present. The reducer canonicalises only on a definitely-True result, so an Unknown (undecidable) comparison leaves the operands in authoring order. Total-ness is the caller's obligation (Jlt: asserted downstream), not checked here.
concept	dedekind::category::IsDefaultMonadTag
concept	dedekind::category::IsPreTransformation
	The raw family of components.
concept	dedekind::category::IsTwoMorphism
	The bridge between two specific Functors.
concept	dedekind::category::IsNaturalTransformation
	A family of components, one per object, whose square commutes at every arrow of the source: \(\alpha_Y \circ F(f) = G(f) \circ \alpha_X\) for each \(f : X \to Y\), read at an arbitrary arrow of the source category's one arrow type, not only at its identities, where every family passes.
concept	dedekind::category::IsDiscreteCategory
concept	dedekind::category::IsPotential
	Structural isomorphism for "Maybe-like" species.
concept	dedekind::category::IsPartialMagma
	A textbook-aligned partial binary algebra.
concept	dedekind::category::IsPartialAssociative
	The Kleene Associativity Law.
concept	dedekind::category::HasPartialIdentity
	Existence of a Neutral Element in a Partial Universe.
concept	dedekind::category::IsPartialSupportClassifier
	Characteristic morphism χ: T -> Ω_K3 for partial support.
concept	dedekind::category::IsPartialSemigroup
concept	dedekind::category::IsPartialMonoid
concept	dedekind::category::IsPartialLoop
	A Partial Monoid with local invertibility on support.
concept	dedekind::category::IsPartialCommutativeSemigroup
concept	dedekind::category::IsPartialGroup
concept	dedekind::category::IsPartialAbelianGroup
concept	dedekind::category::IsMonad
concept	dedekind::category::IsComonad
	The Unified Comonadic Proof: Co-Kleisli Action as Contextual Being.
concept	dedekind::category::IsOckhamAlgebra
	The IsOckhamAlgebra Concept (The Algebraic Signature of Truth).
concept	dedekind::category::HasLogicalOperators
	Pure syntactic shape: T supports the logical operators &&, ||, ! with closed results.
concept	dedekind::category::IsΩ
	A truth-object: a type that can serve as the classifier Ω for a logical species.
concept	dedekind::category::IsPst
	A truth-object that is a bounded chain: an IsΩ classifier whose values are totally ordered.
concept	dedekind::category::LogicalMap
	A callable Pred that maps T -> Ω for some IsΩ Ω. Captures the notion of a predicate valued in an arbitrary logic species.
concept	dedekind::category::IsClassifierAnswer
	T is a classifier answer: it names its species.
concept	dedekind::category::LiftsTo
concept	dedekind::category::HaveLogicJoin
concept	dedekind::category::LiftableInto
	T can be lifted into To's answers: it already is one, or it is a classifier answer whose species' registered embedding into To accepts it and lands in To::Ω (a Truth<L> wrapper is not an L::Ω and is refused).
concept	dedekind::category::IsDeMorganAlgebra
	The committed algebraic tower for the truth objects (#901).
concept	dedekind::category::IsBoundedDeMorganChain
	A De Morgan algebra whose truth carrier Ω is totally ordered; by the chain-normality theorem this is automatically a Kleene lattice.
concept	dedekind::category::IsBooleanLogic
	A bounded De Morgan chain whose reflection is a genuine complement (a∧¬a=⊥, a∨¬a=⊤); on a chain this forces the 2-element case 𝔹.
concept	dedekind::category::IsThinCategory
	A category in which every hom-set has at most one morphism.
concept	dedekind::category::IsSymmetric
	Formal verification: Rel(a, b) ⇔ Rel(b, a).
concept	dedekind::category::IsEquality
	Rel on T is equality of values (the diagonal).
concept	dedekind::category::IsChainDecidedSymmetric
	Symmetry, stated once for every relation on a walkable chain.
concept	dedekind::category::IsEquivalence
	A binary relation on T that is reflexive, symmetric, and transitive — the textbook equivalence-relation axioms.
concept	dedekind::category::IsHashFunction
	A callable h on T whose codomain is std::size_t — i.e. an arrow T → size_t.
concept	dedekind::category::IsQuery
	A query: a range whose elements are Maybe, each present or a hole.
concept	dedekind::category::IsPrefixKernel
	A kernel on the non-empty prefixes of a text: an arrow out of them, a coKleisli arrow of the history comonad, whose answer at a position may read all that came before it and nothing after.
concept	dedekind::category::IsInvolution
	Stated in arrow language: F is an endomorphism on the object T (IsEndomorphism, domain and codomain T — applying it twice returns to the domain) carrying the certificate \(f \circ f = \mathrm{id}_T\). T defaults to the arrow's domain; a bare callable names it. The object may be presented by many types (morphism__Objects_And_Their_Presentations), so the complement on \(\mathrm{Sub}(T)\) is an involution here, through this one concept.
concept	dedekind::category::IsAntiHomomorphism
	A map on T that reverses Op, \(f(a \cdot b) = f(b) \cdot f(a)\): a homomorphism into the opposite, Opposite<Op>, read off the homomorphism certificate rather than declared apart.
concept	dedekind::category::IsDagger
	The \(\dagger\)-category surface built on IsInvolution: IsDagger, the named intermediate IsIsometry, and IsUnitary — where "the converse is the inverse" (bijective relation) and "the transpose is the inverse" (orthogonal matrix) are one theorem.
concept	dedekind::category::IsIsometry
	A singleton morphism-carrier F (its default value is the arrow) whose dagger is a left inverse: the named non-linear intermediate (Heunen & Vicary). For a value-level carrier, use the is_isometry predicate instead.
concept	dedekind::category::IsUnitary
	A singleton morphism-carrier whose dagger is its inverse (isometry and coisometry) — a dagger-iso, \(f^\dagger = f^{-1}\). Hence an IsIsomorphism once lifted into the arrow surface (follow-up).
concept	dedekind::category::IsKleisliTriple
	A Kleisli triple ⟨T, η, (−)*⟩ (Manes), the monad in its extension form: the unit and bind, their laws certified by is_kleisli_triple.
concept	dedekind::category::IsCoKleisliTriple
	A co-Kleisli triple ⟨W, ε, (−)†⟩, the comonad in its extension form: the counit and extend, their laws certified by is_cokleisli_triple.
concept	dedekind::category::IsFrobenius
	A Frobenius monad (Street): a Kleisli and a co-Kleisli triple on one functor whose μ and δ satisfy the Frobenius law, certified by is_frobenius_monad.
concept	dedekind::category::HasKleisliBindOperators
	A monadic carrier MA supports Kleisli bind, >>=, with a Kleisli arrow F; >> composes arrows and nothing else.
concept	dedekind::category::HasComonadicExtendOperators
	A comonadic carrier WA supports comonadic extend, <<=, with a co-Kleisli arrow F.
concept	dedekind::category::HasArrowDereferenceOperator
	Syntactic check: m.operator->() compiles for M.
concept	dedekind::category::IsKleisliDeref
	M exposes operator-> and the carrier site has declared it as Kleisli dereference / comonadic extract (Mac Lane CWM §VI; Wadler 1992).
concept	dedekind::category::IsKleisliArrow
	An arrow declared to live in the Kleisli category indexed by the monad tag M (constrained by IsDefaultMonadTag).
concept	dedekind::category::IsInitialFAlgebra
	Carrier A is the initial F-algebra for endofunctor F with structure map α.
concept	dedekind::category::IsTerminalFCoalgebra
	Carrier A is the terminal F-coalgebra for endofunctor F with structure map α.
concept	dedekind::category::IsTermNode
	A node of the term functor: a type that exposes its legs.
concept	dedekind::category::Steers
	An algebra that steers the fold at T (Mendler style): it recurses into the legs it chooses by cata itself, instead of the strict fold.
concept	dedekind::category::detail_f_algebra::HasComponentOrders
	Op is a product order with component orders to descend into.
concept	dedekind::category::IsNumericSpecies
concept	dedekind::category::IsLipschitzBoundaryPolicy
	User-provided Lipschitz boundary policy over a numeric species.
concept	dedekind::category::IsNumericHoleClassifier
	A characteristic morphism χ: T -> Ω_K3 for numeric support.
concept	dedekind::category::IsLatticeCategory
	A posetal category that is both filtered and cofiltered, with joins and meets given by the algebraic lattice operations.
concept	dedekind::category::IsBoundedLatticeCategory
	A lattice category that has a designated bottom (initial) and top (terminal) element — row 5 of the lattice Form-chain (#698 Slice 4).
concept	dedekind::category::HasLogicSpecies
	The equational laws a lattice concept induces, as compile-time term-reduction rules over the term AST below. Each law is a decomposable, independently-testable part; the assembled reducer (:lattice_term) applies exactly the laws the supplied carrier proves. The richer the carrier's structure (a bounded chain is the sweet spot; bool the optimal witness), the more laws fire and the further a term collapses.
concept	dedekind::category::IsSpeciesTaggedArrow
	An arrow that names its logic species and answers in it: Cod.
concept	dedekind::category::SameCarrier
	Do both operands live in the same, known carrier? The boundary laws require this so a bound of one carrier (e.g. an int ⊤) is never applied as the unit / annihilator of a term whose other operand lives in a different carrier: a mixed-carrier term (⊤ᵢₙₜ ∧ bool-leaf) fails closed. Because the carrier is read via carrier_of, the laws still apply to an arbitrary same-carrier composite subterm (⊤∧X=X even when X is an un-collapsed Meet / Join), not only to leaves. (The glb/lub law forces a shared carrier through OrderComparable; this is its boundary-law counterpart.).
concept	dedekind::category::IsIdempotentLeaf
	T's values are determined by its type, so a type-only lattice law (X∧X=X idempotence, a∧¬a=⊥ complement) collapses soundly on it: two same-type instances are necessarily the same value. A runtime-stateful leaf (say a Singleton holding a value, or a predicate with an expected field) is not idempotent, so those laws must not fire on it, else Meet{S{7},¬S{3}} would wrongly collapse to ⊥. This is the value-safety gate the type-level reducer shares with the value-first :lattice_term reducer (#922). Recursive over Meet / Join / Not through idempotent_leaf_v.
concept	dedekind::category::OrderComparable
	Can A and B be compared in the injected order Ord, at compile time? Both must expose ::value of one carrier type T that is IsPosetal under Ord's resolved relation, and that relation must be default-constructible and constexpr-callable on those values. A registered-but-runtime-only or stateful order therefore fails this guard and the glb/lub collapse stays inactive (fail-closed) rather than hard-erroring.
concept	dedekind::category::IsInvolutiveEndofunctor
	Involutive endofunctor concept — an endomap F : T → T with F² ≅ Id.
concept	dedekind::category::IsHeytingLatticeCategory
	A bounded lattice category whose lattice exponentials are witnessed by :cartesian::IsExponential — row 6 of the lattice Form-chain (#698 Slice 6).
concept	dedekind::category::IsBooleanLatticeCategory
	A Heyting lattice category whose complement is an involutive endofunctor satisfying the Boolean complement laws — row 7 of the lattice Form-chain (#698 Slice 7).
concept	dedekind::category::IsSubobjectFamilyMember
	Compile-time meeting-point pins (#698 Slice 10) — three structurally distinct carriers at the same Form-chain rows.
concept	dedekind::category::IsSubobjectLattice
	A type S is the carrier of a subobject lattice over S::Domain, with lattice structure induced pointwise from the classifier S::logic_species::Ω.
concept	dedekind::category::IsBooleanSubobjectLattice
	The Form-chain ≤ relation on a subobject lattice is derivable from meet:
concept	dedekind::category::IsByteText
	A contiguous text of bytes, from a const value, as a block of a scan reads it and as where reads a window.
concept	dedekind::category::IsRetractableArrow
	A monic arrow that ships with a structurally-known retract, a partial inverse retract(f) : Cod<F> → Maybe<Dom<F>>, discoverable via ADL on F.
concept	dedekind::category::Presents
	S presents the object C: a value convertible to C (the default: the object is one value type), or a type the object names (C::presents).
concept	dedekind::category::IsArrow
	A type that knows its own Domain (A) and Codomain (B), objects it maps between: called at the domain's representative, its result presents the codomain (morphism__Objects_And_Their_Presentations).
concept	dedekind::category::IsSmallCategoryShape
	The structural prefix of IsSmallCategory (:small): a type naming an ::Arrow, a ::Species and an ::Id, the shape of a category, without its behavioural axioms (id_c, composition closure). IsSmallCategory itself cannot be named here, since :small imports :morphism. It tells a category apart from an object that merely exposes Domain / Codomain aliases: a Path<T>, a sequence \(\mathbb{N} \to T\), is an arrow and an object of Set, not a category (#525).
concept	dedekind::category::IsEndomorphism
	Proposition: A Morphism where Domain ≡ Codomain (f: A -> A).
concept	dedekind::category::IsIdentityArrow
concept	dedekind::category::IsIsomorphism
	An Arrow f: A -> B with a guaranteed Inverse g: B -> A.
concept	dedekind::category::IsConstantArrow
	An arrow known to be constant: every argument to one value.
concept	dedekind::category::IsMonicArrow
	An arrow declared to be a monomorphism (ι: A ↣ B).
concept	dedekind::category::IsEpicArrow
	An arrow declared to be an epimorphism (π: A ↠ B).
concept	dedekind::category::IsMagmaHomomorphism
	A map on T declared to carry Op to Op2: \(f(a \odot b) = f(a) \circledast f(b)\).
concept	dedekind::category::PreservesUnit
	A map on T carries the unit of Op to the unit of Op2, \(f(e) = e'\), computed at the one unit: the comparison is a template argument, so a map that is no constexpr function object is refused rather than an error. The unit half of a monoid homomorphism, and of a homomorphism of any signature whose operations have units.
concept	dedekind::category::IsBijectiveArrow
	An arrow declared to be both a monomorphism (ι: A ↣ B) and an epimorphism (π: A ↠ B), i.e. an isomorphism of sets (A ≅ B).
concept	dedekind::category::IsInjective
	Set-theoretic synonym for IsMonicArrow — an arrow is injective iff distinct inputs yield distinct outputs (f(x) == f(y) → x == y).
concept	dedekind::category::IsSurjective
	Set-theoretic synonym for IsEpicArrow — an arrow is surjective iff every codomain element has a preimage (∀ b ∈ B ∃ a ∈ A. f(a) == b).
concept	dedekind::category::IsBijective
	Set-theoretic synonym for IsBijectiveArrow — an arrow is bijective iff it is both injective and surjective, i.e. a set-theoretic isomorphism A ≅ B.
concept	dedekind::category::HasArrowComposeOperators
	Two arrow types F, G compose via >> .
concept	dedekind::category::IsPredicate
	The Predicate Morphism: the DSL's membership test, i.e. the characteristic arrow \(\chi_A : A \to \Omega\).
concept	dedekind::category::IsCharacteristic
	Categorical alias for a Predicate mapping to Ω: the characteristic arrow \(\chi_A : A \to \Omega\) that classifies a subobject (a set).
concept	dedekind::category::IsDecidableCharacteristic
	The Boolean refinement of IsCharacteristic: a membership test valued in the dominance Σ, i.e. \(\chi_A : A \to \Sigma\) with \(\Sigma = \Omega\)-decided \(= @c bool\).
concept	dedekind::category::IsDominanceInclusion
	The Rosolini inclusion arrow \(\iota : \Sigma \hookrightarrow \Omega\): a map between truth-objects out of the decided fragment.
concept	dedekind::category::IsSieve
	Signature-level witness for a sieve of arrows into an object.
concept	dedekind::category::IsGrothendieckTopology
	Signature-level witness for Grothendieck coverage rules over sieves.
concept	dedekind::category::IsBundleProjection
	A projection morphism π : E -> B for a bundle candidate.
concept	dedekind::category::IsFiberBundle
	Signature-level witness for a fiber bundle over a base species.
concept	dedekind::category::IsSubobject
	The categorical witness of a monomorphism ι: S ↣ A — a characteristic morphism χ: A → Ω together with its inclusion.
concept	dedekind::category::IsLSet
	An L-set: a subobject of a carrier with \(\chi : X \to L\) into a named bounded chain \(L\) (Codomain = L::Ω). The carrier is asked for copies (std::semiregular), not for a decidable ==: the equality of sets is the Rice cycle (#970), not a trait of the carrier, so the relations of a hom-set are a carrier too (𝔸<RelExpr>, #1045). An ETCS set asks decidable equality itself (IsSet, whose classifier construction needs it), as IsArrow asks an archetype of its domain rather than a value type (archetype_t). Pst is asked of the species (an Ockham algebra whose Ω is totally ordered), not of the bare Ω, so a Chain<int> set (Ω = int) qualifies while a bare int never does. The chain is the registered total order (IsTotalOrder: reflexive, transitive, antisymmetric, comparable), not the syntactic std::totally_ordered, so an Ω without certified order laws (a raw float, whose NaN breaks reflexivity) is refused honestly.
concept	dedekind::category::IsFiniteChain
	A carrier that is a finite chain by its representation: totally ordered and either a machine integer or an enumeration (both finite by construction). bool, Ternary, int qualify; Cardinality and the dense carriers do not.
concept	dedekind::category::IsFiniteLSet
	The Pst fragment: an L-set whose carrier is a finite chain (IsFiniteChain), so χ is a finite table and normalisation by evaluation is complete. Products of finite chains follow with IsProduct.
concept	dedekind::category::IsQuotient
	The categorical witness of a regular epimorphism q: A ↠ Q — the dual of IsSubobject.
concept	dedekind::category::IsPredicatePair
	Two predicates over one object, answering in one species: the operand sort of the predicate combinators below, which close on IsPredicate. Named so the set grammar's && / || (sets) can take exactly the other pairs of terms (relational fragments, mixed terms, the structured collapse) without overlapping these.
concept	dedekind::category::IsTruthObject
	Ω may carry a relation's answer in the laws below: it has a top ⊤, the value a law asserts (reflexivity is rel(a, a) = ⊤). bool (top true) is the default; Ternary names its Ω::True, a value type with a species (Percentage, the bounded chains) finds it on the species. A statement of intent, not a certificate: the laws come before logic, so the truth objects are only certified downstream (:logic, IsΩ).
concept	dedekind::category::IsReflexive
	Formal verification of the identity relation.
concept	dedekind::category::IsTransitive
	Formal verification: (a ≤ b ∧ b ≤ c) ⇒ a ≤ c.
concept	dedekind::category::IsAntisymmetric
	Formal verification: (a ≤ b ∧ b ≤ a) ⇒ a = b.
concept	dedekind::category::IsConnex
	Formal verification: a ≤ b ∨ b ≤ a.
concept	dedekind::category::SupInfOperand
	A carrier on which Sup / Inf (and max / min) are a genuine, usable value op: totally ordered (for <) and copy-constructible (the winner is returned by value). This is the CALL gate: Sup{}(1.0, 2.0) is a valid call that returns a value, so raw floats are not excluded here; only the lattice laws fail on them (see SupInfLattice).
concept	dedekind::category::SupInfLattice
	A carrier on which max / min (and Sup / Inf) are honest lattice ops: usable (SupInfOperand) and carrying a certified order.
concept	dedekind::category::IsWalkableChain
	Rel is a stateless relation on a discrete bounded chain T on which a law of Arity variables can be decided: a step (successor, by argument-dependent lookup, as for HasNNOStep), a least and a greatest value (the identities of Sup and Inf), the top reached from the bottom within chain_walk_budget, and nᴬʳⁱᵗʸ within law_evaluation_budget, all as constant expressions (what cannot be evaluated at compile time is simply not decided here, rather than an error).
concept	dedekind::category::IsChainDecidedReflexive
	Each law, stated once for every relation on a walkable chain: the certificate the concept reads is the law over the whole chain, for ≤, ≥, ==, or any stateless relation, decided and never registered per operator. A carrier that answers through its own member keeps that answer; a law the compiler cannot evaluate is not decided here. Exported conditions, so a rule elsewhere can yield to these.
concept	dedekind::category::IsChainDecidedAntisymmetric
concept	dedekind::category::IsChainDecidedConnex
concept	dedekind::category::IsChainDecidedTransitive
concept	dedekind::category::IsPartRelation
	Verifies that a binary operator satisfies Leśniewski's mereological axioms.
concept	dedekind::category::IsPartialOrder
	Named stage for the partial-order maturity level of parthood.
concept	dedekind::category::IsTotalOrder
	Linear/total refinement of IsPartialOrder.
concept	dedekind::category::IsPartOfRelation
	Minimal core part-whole relation yielding Omega.
concept	dedekind::category::IsMereologicalJoinMagma
	Stage 0 for join-like algebra: closure only.
concept	dedekind::category::IsMereologicalMeetMagma
	Stage 0 for meet-like algebra: closure only.
concept	dedekind::category::IsMereologicalJoinSemigroup
	Stage 1 for join-like algebra: magma + associativity.
concept	dedekind::category::IsMereologicalMeetSemigroup
	Stage 1 for meet-like algebra: magma + associativity.
concept	dedekind::category::IsMereologicalMeetBand
	Non-commutative meet-like operation (associative + idempotent).
concept	dedekind::category::IsMereologicalJoinBand
	Non-commutative join-like operation (associative + idempotent).
concept	dedekind::category::IsAbsorptive
	Mutual absorption and internal idempotency for a pair of operations.
concept	dedekind::category::IsMereologicalSkewLattice
	Non-commutative lattice-style operations (skew lattice fragment).
concept	dedekind::category::IsMereologicalLatticeOperations
	Compatibility lattice alias over the skew core + absorption.
concept	dedekind::category::IsMereologicalDistributiveLatticeOperations
	Mature distributive stage: lattice operations with mutual distribution.
concept	dedekind::category::HasExtrema
	Structural requirement for Dedekind completeness witnesses.
concept	dedekind::category::IsMereologicalCutCandidate
	Transitional bridge contract for the soft-to-hard structural cut.
concept	dedekind::category::Parthood
	Skeletal part-whole contract at the concept level.
concept	dedekind::category::IsSpecies
	Formal verification that a type has been registered in the Atlas.
concept	dedekind::category::HasTotalProduct
	Whether T's product is defined on all of T: a word narrower than int multiplies after promotion to int, and the largest product must fit it. unsigned char's does (255 · 255); unsigned short's does not (65535 · 65535 overflows int, undefined as -INT_MIN is), so it is refused as int is. Decided by the compiler: undefined behaviour is no constant expression. Unsigned words only: there the product grows with its factors, so the largest is the one that may overflow, and numeric_limits names it (a type without limits has max() == T{}, and the probe would check only 0 · 0).
concept	dedekind::category::IsTransfinite
concept	dedekind::category::IsFinite
concept	dedekind::category::IsAssociative
concept	dedekind::category::IsCommutative
concept	dedekind::category::IsDistributive
	The "Glue" of the Ring: a * (b + c) = a*b + a*c.
concept	dedekind::category::IsIdempotent
concept	dedekind::category::IsPosetal
	A Category where morphisms are governed by a specific Logic Species (Ω).
concept	dedekind::category::IsTotallyOrderedPosetal
	Posetal refinement where the underlying order is total/linear.
concept	dedekind::category::IsOrderMeetSemilattice
	Order-theoretic meet-semilattice as a commutative refinement.
concept	dedekind::category::IsCertifiedOrderMeetSemilattice
	Trait-certified meet-semilattice (associative + idempotent + commutative).
concept	dedekind::category::IsOrderJoinSemilattice
	Order-theoretic join-semilattice as a commutative refinement.
concept	dedekind::category::IsCertifiedOrderJoinSemilattice
	Trait-certified join-semilattice (associative + idempotent + commutative).
concept	dedekind::category::IsOrderLatticeOperations
	Order-theoretic lattice operations as commutative + absorptive refinement over upstream mereological lattice operations.
concept	dedekind::category::IsCertifiedOrderLatticeOperations
	Trait-certified lattice operations (commutative semilattices + absorption).
concept	dedekind::category::IsOrderDistributiveLatticeOperations
	Distributive lattice refinement over IsOrderLatticeOperations.
concept	dedekind::category::IsCertifiedOrderDistributiveLatticeOperations
	Trait-certified distributive lattice refinement.
concept	dedekind::category::IsPathProjection
	Projection contract used by check_path to map objects into an orderable relation carrier.
concept	dedekind::category::IsMonotone
	An arrow F declared to be order-preserving with respect to the ambient order relation Op.
concept	dedekind::category::IsAntiMonotone
	An arrow F declared to be order-reversing with respect to the ambient order relation Op.
concept	dedekind::category::IsVariant
	An arrow with a definite variance: order-preserving (IsMonotone) or order-reversing (IsAntiMonotone). The leg-shape of a Galois connection, whose adjoints are always one or the other. Mirrors :limit::IsBoundaryObject's "X @c || @c dual" disjunction shape.
concept	dedekind::category::IsOrderIsomorphism
	An arrow that is both an order-preserving map and a bijection.
concept	dedekind::category::IsOrderAntiIsomorphism
	An arrow that is both an order-reversing map and a bijection.
concept	dedekind::category::HasDomain
	A type that names its domain: Dom<F> is formed. The guard under which IsInvolution<F> may be asked at all.
concept	dedekind::category::IsImageOf
	S realises the image of arrow F as a Subobject of Cod<F> — the mono side of the (regular epi, mono) factorisation system pinned in :factorisation.
concept	dedekind::category::IsCoequalizer
	The categorical dual of IsEqualizer — a Quotient of Cod<F> equating two parallel arrows F, G.
concept	dedekind::category::WitnessesFirstIso
	Connector witnesses the First Isomorphism Theorem at homomorphism F.
concept	dedekind::category::HasAdjunctionShape
	Structural shape: F and U have the categorical signature of an adjoint pair F ⊣ U — F : 𝒟 → 𝒞 (left, free) and U : 𝒞 → 𝒟 (right, forgetful).
concept	dedekind::category::IsFreeFunctor
	Directional alias: F is the left adjoint of an adjunction F ⊣ U. Names the free direction — F sends an object d : 𝒟 to its free construction F(d) : 𝒞 (the universal recipient under U).
concept	dedekind::category::IsForgetfulFunctor
	Directional alias: U is the right adjoint of an adjunction F ⊣ U. Names the forgetful direction — U drops the structure that distinguishes 𝒞 from 𝒟 (e.g., U_Ring→Rig forgets that you can do −).
concept	dedekind::category::IsUnitOfAdjunction
	Structural shape: η is the unit of an adjunction F ⊣ U — a natural transformation id_𝒟 ⇒ U ∘ F.
concept	dedekind::category::IsCounitOfAdjunction
	Structural shape: ε is the counit of an adjunction F ⊣ U — a natural transformation F ∘ U ⇒ id_𝒞. Dual of IsUnitOfAdjunction.
concept	dedekind::category::IsAdjunction
	A typed unit/counit witness relating a left and right functor.
concept	dedekind::category::IsCovariantFunctor
	A covariant functor between posetal categories: an order-PRESERVING arrow. This is IsMonotone read categorically (a monotone map is a functor of posets that preserves the direction of composition), the documented covariant pole of functor variance (#908).
concept	dedekind::category::IsContravariantFunctor
	A contravariant functor between posetal categories: an order-REVERSING arrow (IsAntiMonotone read categorically). The contravariant pole; inhabited by the negation NegationArrow ¬ and any Compose that mixes one covariant with one contravariant leg.
concept	dedekind::category::IsVariantFunctor
	A functor between posetal categories with a definite variance: covariant or contravariant. This is the "@c IsFunctor parametrized with @c IsVariant" umbrella whose poles are IsCovariantFunctor and IsContravariantFunctor, and exactly the leg-shape a Galois connection's adjoints must share (matched variance, below).
concept	dedekind::category::IsOrderEmbedding
	An order-preserving embedding: a monic, order-preserving arrow of one ordered set into another. Such an embedding is a covariant functor between the two posetal categories, so IsCovariantFunctor is a conjunct — the classification is derived from the two legs (IsEmbeddingFunctor && IsMonotone), not re-declared per carrier (#908).
concept	dedekind::category::IsGaloisConnection
	Structural shape: F and G form a Galois connection F ⊣ G in a posetal setting — the simplest adjunction. Both are monotone arrows; F : P → Q and G : Q → P with the source/target carriers crossed (so F's Codomain matches G's Domain and vice versa). The universal-property test, for monotone legs
concept	dedekind::category::IsClosureOperator
	Structural shape: C is a closure operator on a poset P — an arrow C : P → P that is idempotent (C(C(x)) = C(x)), monotone (x ≤ y ⇒ C(x) ≤ C(y)), and extensive (x ≤ C(x)) for all x.
concept	dedekind::category::IsLeftAction
	The shape of a left action (S ⟳ M), \(S \times M \to M\), scalar first, as a module's: its laws are the certificate a concept above it reads (is_linear_action for a semimodule). A left action of a monoid \(M\) is a right action (IsRightAction) of its opposite, Opposite<Op> (:involution), and over a commutative monoid the two coincide.
concept	dedekind::category::IsSemimodule
	A commutative monoid M on which the semiring S acts linearly.
concept	dedekind::category::HasCountingAction
	The counts act on (T, Op) in one step, by a law: the semimodule laws or idempotence.
concept	dedekind::category::IsRightAction
	H is a right action \(M \times S \to M\) of the monoid (S, Op) that acting_monoid<H> names: M is a right S-set (Mac Lane and Moerdijk), an S-act (Kilp, Knauer and Mikhalev, Monoids, Acts and Categories). A left action is a right action of the opposite, Opposite<Op>.
concept	dedekind::category::IsIntegerChain
	A chain with integer arithmetic: a discrete total order, locally finite (every bounded interval is finite), so a distributive lattice under min and max, with the NNO's step and the arithmetic operators as a shape. Finite on a machine word, unbounded for a bignum. Not a ring: int's overflow is undefined and a cardinal may saturate at \(\aleph_0\); the ring is IsRing's to claim.
concept	dedekind::category::IsCountWord
	A word of the counts: an integer chain whose arithmetic wraps at its cyclic order, the unsigned integers but bool, and none narrower than int, whose products promote to a signed int that may overflow. std::size_t is the default throughout.
concept	dedekind::category::IsFiniteChainSequence
	A sequence on finite chains: an arrow out of the counts, read along a chain of them (the Jlt paper's Figure 2, its vertical arrows). The chain is finite by its descent and ordered by its step, so the sequence needs no set concept; its laws, a period or an order kept or reversed, are laws of the composite chain >> f, and the folds read them (#1133).
concept	dedekind::category::IsExponential
	Categorical exponential object B^A — generalised structural recogniser of "eval morphism via call expression" (#698 Slice 6).
concept	dedekind::category::IsArrowExponential
	An exponential E : A → B that also satisfies the project's morphism vocabulary (IsArrow with matching Domain / Codomain typedefs). #706.
concept	dedekind::category::IsCoproduct
	Categorification of std::variant<A, B> as the categorical coproduct (A + B).
concept	dedekind::category::IsCartesianClosed
	A Category equipped with Terminal Objects, Products, and Exponentials.
concept	dedekind::category::IsProductCategory
	A category whose Species is a categorical product (std::pair).
concept	dedekind::category::IsBinaryRelation
	A type R is a binary relation A × B → bool if it is callable on A and B and yields a boolean.
concept	dedekind::category::IsBinaryFunction
	A binary relation R ⊆ A × B is a function when it is left-total AND right-unique.
concept	dedekind::category::IsDirectedGraph
	A homogeneous binary relation R ⊆ V × V on a vertex set V is a directed graph: each ordered pair (u, v) with R(u, v) == true is an edge.
concept	dedekind::category::IsUndirectedGraph
	A directed graph R is undirected when its relation is symmetric: R(u, v) iff R(v, u).
concept	dedekind::category::IsCongruence
	A homogeneous binary relation R on a carrier V is a congruence w.r.t. operation Op when it is an equivalence relation and respects Op.
concept	dedekind::category::HasSubscriptOperator
	Syntactic check: s[i] compiles for Seq, Idx.
concept	dedekind::category::IsEvalArrow
	Seq exposes operator[Idx] and the carrier site has declared it as the CCC eval counit (Mac Lane CWM §IV.6).
concept	dedekind::category::IsRegularEpi
	An arrow E is a regular epi when it is an epi and registered as the coequalizer of some parallel pair.
concept	dedekind::category::IsRegularMono
	Dual of IsRegularEpi: an arrow M is a regular mono when it is a mono and the equalizer of some parallel pair.
concept	dedekind::category::IsFactorisationSystem
	Category C admits the canonical (regular epi, mono) factorisation system. Form-chain row 6 (#718).
concept	dedekind::category::IsRegularCategory
	Category C satisfies the regular-category axioms. Pinned for Set and (transitively) every topos.
concept	dedekind::category::IsExactCategory
	Category C satisfies the exact-category axioms. Sollbruchstelle landing site.
concept	dedekind::category::IsCopy
	: the DIAGONAL notion Δ:A→A×A --- an arrow whose Codomain is the square of its Domain (the comonoid comultiplication / fan-out). Copy is the canonical MODEL; this concept is the matchable "diagonal" handle. Purely structural: it names the crossed A→A×A signature, not that the map is a↦(a,a) (that is Copy's own obligation). Cartesian only: the non-cartesian ⊗ setting needs the carrier generalized past std::pair (#951); a type carrying more than one arrow reading needs the dom/cod contract (#952).
concept	dedekind::category::IsMerge
	: the FOLD notion Δ†:A×A→A --- an arrow whose Domain is the square of its Codomain (the comonoid dagger / binary combiner). Merge<A,Meet> is the canonical MODEL; this concept is the matchable handle. Purely structural: it names the A×A→A signature, so a PROJECTION π:A×A→A also satisfies it (the shape cannot tell a fold from a projection, the same honesty gap as glb-vs-lub). Same seams as IsCopy: carrier past std::pair (#951); the multi-reading dom/cod contract (#952).
concept	dedekind::category::IsMeetAsRightAdjoint
	The STRUCTURAL shape of "the meet @c ∧ is the right adjoint of the diagonal @c Δ" (Δ⊣∧): the reified theory this slice postulates as a type-check.
concept	dedekind::category::IsTensor
	: the structural shape of the parallel product ⊗ --- an arrow whose Domain AND Codomain are product objects (the arrow-half of the product bifunctor). Tensor<R,S> is the canonical MODEL; this concept is the matchable handle. Cartesian only: the non-cartesian monoidal ⊗ (LA outer product) needs the carrier generalized past IsProduct (#951); a type with >1 arrow reading needs the dom/cod contract (#952).
concept	dedekind::category::HasAxiom1Composition
	ETCS axiom 1 witness: composition is available for ambient arrows.
concept	dedekind::category::HasAxiom2Identity
	ETCS axiom 2 witness: identity arrow acts neutrally on A.
concept	dedekind::category::HasAxiom3TerminalObject
	ETCS axiom 3 witness: terminal object 1 is present.
concept	dedekind::category::HasAxiom4WellPointedness
	ETCS axiom 4 witness: membership is evaluation through the carrier-as-characteristic-morphism. Post-#681 structural refactor: IsSubobject already requires the structural call shape { s(a) } -> IsΩ, so the membership-as-evaluation reading lands on the IsSubobject witness itself.
concept	dedekind::category::HasAxiom5CartesianProduct
	ETCS axiom 5 witness: products exist for ambient species A.
concept	dedekind::category::HasAxiom6Exponentiation
	ETCS axiom 6 witness: exponentials B^A exist (here A^A witness). Uses the named IsArrowExponential refinement (#706) rather than the ad hoc IsExponential && IsArrow combination that lived here previously.
concept	dedekind::category::HasAxiom7SubobjectClassifier
	ETCS axiom 7 witness: every set is represented by a subobject.
concept	dedekind::category::HasAxiom7ClassifierNaturalityWitness
	Optional naturality witness for Axiom 7 classifier behavior.
concept	dedekind::category::HasAxiom8EmptySet
	ETCS axiom 8 witness: initial object 0 is present.
concept	dedekind::category::HasAxiom9NNO
	ETCS axiom 9 witness: arithmetic species atlas exposes ℕ witness.
concept	dedekind::category::IsSplitEpicPair
	Structural witness of a split epimorphism e with section s.
concept	dedekind::category::HasAxiom10ChoiceSplitEpicWitness
	Axiom 10 (choice) support via an explicit split-epi witness shape.
concept	dedekind::category::HasAxiom10ChoiceSplitEpicLawSurface
	Axiom 10 semantic-law surface (split-epi shape + equality codomain).
concept	dedekind::category::HasAxiom7PullbackReindexingDefinitionalSurface
	Axiom 7 definitional reindexing witness surface.
concept	dedekind::category::HasAxiom10PowerObjectLattice
	ETCS axiom 10 witness: power-object lattice completeness.
concept	dedekind::category::HasETCSAxioms
	Diaconescu's classical direction (#698 Slice 9 review).
concept	dedekind::category::IsSet
	ETCS set: a carrier satisfying the 10 ETCS axioms AND admitting the canonical Set-CCC witness over its ambient species.
concept	dedekind::category::IsLocallySmallCategory
	Value-level locally-small witness: the Hom-collection of Cat is a set in the metatheory.
concept	dedekind::category::IsSmallCategory
	A point-free, morphism-only reification of a Category.
concept	dedekind::category::IsPullback
	The apex of a pullback square over the cospan f: X ⟶ Z, g: Y ⟶ Z: a subobject carrying the two projection legs π₁ ⟶ X, π₂ ⟶ Y.
concept	dedekind::category::IsEqualizer
	The kernel of a parallel pair (f, g: A ⟶ B).
concept	dedekind::category::IsKernelPair
	The pullback of an arrow F against itself — the equivalence relation "have the same F-image" on Dom<F>.
concept	dedekind::category::IsPushout
	The categorical dual of IsPullback: the apex of a pushout square over the span f: Z ⟶ X, g: Z ⟶ Y, carrying the two coprojection colegs ι1: X ⟶ P, ι2: Y ⟶ P.
concept	dedekind::category::IsParallelPair
	F and G are a parallel pair of arrows — shared Dom and shared Cod.

Classes
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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 ℤ. More...
struct	dedekind::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\). More...
struct	dedekind::category::Prior< N >
	The destructor \(\langle \text{is}\;Z?,\, P\rangle : N \to 1 + N\): nothing at zero, else the predecessor. More...
struct	dedekind::category::is_functorial< F >
	Trait: F preserves identities and composition, \(F(\mathrm{id}) = \mathrm{id}\) and \(F(f \gg g) = F(f) \gg F(g)\): the functor laws, a certificate as is_involutive and commutes are, primary std::false_type. A type cannot show them, since \(F(f \gg g)\) and \(F(f) \gg F(g)\) are different types that denote one arrow; a functor that lifts each arrow letterwise, elementwise or not at all declares it, and a composite of functors derives it. More...
struct	dedekind::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. More...
struct	dedekind::category::TupleMap< T, F >
	f on the one element of a one-tuple: the one-tuple functor's action on an arrow. More...
struct	dedekind::category::maybe_functor< T >
	The Intensional Functor for Optional (Maybe) values. More...
struct	dedekind::category::tuple_functor< T >
	The Intensional Functor for 1-tuple values. More...
struct	dedekind::category::composite_functor< F, G >
	Composite Functor G . F (Maps CatS -> CatT -> CatU). More...
struct	dedekind::category::f_algebra< Carrier, Functor, Structure >
	A concrete witness for an F-algebra. More...
struct	dedekind::category::f_coalgebra< Carrier, Functor, Structure >
	A concrete witness for an F-coalgebra. More...
struct	dedekind::category::identity_functor< Cat >
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::Acting< H, V, S >
	An element acting: the arrow \(v \mapsto h(v, s)\) on the set the monoid acts on. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::LeftActing< Act, M, S >
	A scalar acting on the left: the arrow \(m \mapsto s \cdot m\) of a semimodule. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::is_periodic< T, Op >
struct	dedekind::category::is_saturating< T, Op >
struct	dedekind::category::is_exact_total< T, Op >
	Path D to totality: the operation is total because the carrier is exact — arithmetic with no rounding, Op(a,b) defined and lossless up to the carrier's out-of-memory tripwire. The archetypes are the exact number fields (Rational = ℚ, QuadraticReal = ℚ(√D)) under + and *. Distinct from the three machine-finite paths, which are total by staying in a bounded range (wrap / stabilise / saturate); an exact carrier is total because its arithmetic is closed and exact. More...
struct	dedekind::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. More...
struct	dedekind::category::is_total_by_construction< T, Op >
	Path E to totality: by construction. Defined below is_total, which it recurses into on the base. More...
struct	dedekind::category::is_total< T, Op >
	The certificate. Op is taken up to cv/ref (a const Inf keys the same registration as Inf). More...
struct	dedekind::category::is_cyclic_group< T, Op >
	Opt-in trait: is (T, Op) a \emph{cyclic} abelian group? More...
struct	dedekind::category::cyclic_order< T, Op >
	The order \(n\) of a cyclic group (its cardinality). More...
struct	dedekind::category::Projection< K >
	The projection π_k: the k-th component of a product. More...
struct	dedekind::category::Projection< 0 >
	The projection out of the one-fold product A¹ ≅ A: the identity arrow (Identity), read at the point's own type. More...
struct	dedekind::category::AnyOperation
	Base-case sentinel for the operation parameter of IsProduct / IsCoproduct. More...
struct	dedekind::category::unit_period< F >
	The trait behind HasUnitPeriod: a sequence whose period is 1 by its type, not only by its value, so that the sum along it needs no fold. A struct, as is_adjoint, so that a downstream partition registers a family by one partial specialisation. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::Factor< N >
	A factor of a count, \(b^e\): a base raised to an exponent. More...
struct	dedekind::category::Cycles< N >
	The cycles of a permutation of positions of one length, and how many there are: one term of its cycle type. More...
struct	dedekind::category::Letters
	A 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"). More...
struct	dedekind::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. More...
struct	dedekind::category::Ranked
	A 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. More...
struct	dedekind::category::Reflection
struct	dedekind::category::SplitMix
	A 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. More...
struct	dedekind::category::RandomLetter
	A random letter by position: the hash, read as a rank in an alphabet. More...
struct	dedekind::category::LetterMap
	An 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. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::LetterMaps
	The letter maps on the bytes as a category: one arrow type, LetterMap, the identity its identity table. More...
struct	dedekind::category::LetterMapsOnWords
	The letter maps on every letter of a word as a category: the image of LetterMaps under the list functor. More...
struct	dedekind::category::PowerFunctor
	The 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. More...
struct	dedekind::category::OnWords< S >
	A transformation of the power functor with one component, a map on the words, the same at every letter. More...
struct	dedekind::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. More...
struct	dedekind::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). More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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.) More...
struct	dedekind::category::length_coherent< S >
	A permutation family coherent across lengths: from n to n + 2 its cycle type gains cycles and changes none. The reversal's is: the longer chain's antitone bijection restricted to the middle is the shorter's, with one more pair outside (antitone_cycle_type). A rotation's follows \(\gcd(n, d)\) and is not. Coherence is naturality: the family is a natural transformation of the powers over the chains and their middle inclusions \(n \hookrightarrow n + 2\) (IsNaturalTransformation, :natural), as it is natural over the letter maps already (power(τ) commutes with it). Sufficient, not necessary: rotate(1) is not coherent, yet its sections' density \(|\Sigma| / |\Sigma|^n\) falls. A struct trait, for a family to register by one specialisation. More...
struct	dedekind::category::density_falls_on_even_lengths< Fam >
	A family of sets of words whose density does not grow along the even lengths. Derived, not registered per family: the powers have density 1; fixing a permutation keeps it at most 1, cycle by cycle; a length-coherent permutation adds cycles from n to n + 2, each at most 1, so the density along the even lengths does not grow (the restriction sites: \(k^j / |\Sigma|^{2j}\) of length \(2j\), k the letters \(\tau^2\) fixes). More...
struct	dedekind::category::Outer< A, B >
	An outer product of two counted tensors, its count the product of theirs. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::Pow2< N >
	\(k \mapsto 2^k\) on the counts, refused past the word: the window of the bit words. More...
struct	dedekind::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\). More...
struct	dedekind::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. More...
struct	dedekind::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}\). More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::is_directed< T, Rel >
	Trait to mark a relation as directed: every pair of elements has an upper bound. More...
struct	dedekind::category::is_codirected< T, Rel >
	Trait to mark a relation as codirected: every pair of elements has a lower bound. More...
struct	dedekind::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). More...
struct	dedekind::category::lattice_less_logic< Less >
struct	dedekind::category::no_leaf_combine
	The 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 ∧/∨. More...
struct	dedekind::category::no_canonical_order
	No order for the reducer to canonicalise by: a carrier without one keeps the residue in its authored order, then combines it. More...
struct	dedekind::category::Reduce< Less, Ord, Combine >
struct	dedekind::category::maybe_monad_tag
struct	dedekind::category::identity_monad_tag
struct	dedekind::category::tuple_monad_tag
struct	dedekind::category::identity_transformation< F >
	The Identity Natural Transformation for Functor F. More...
struct	dedekind::category::vertical_composition< Α, Β, F, G, H >
	Vertical composition of two 2-morphisms (β . α). More...
struct	dedekind::category::horizontal_composition< Α, Β, F, F_prime, G, G_prime >
	Horizontal composition (Godement product). More...
struct	dedekind::category::ConstantMorphism< A, B >
	The Constant Morphism f: A -> B. More...
struct	dedekind::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)). More...
struct	dedekind::category::DiscreteCategory< T >
	DiscreteCategory realization using the Identity Morphism. Lifts a species T into a category where every arrow is the Identity<T>. More...
struct	dedekind::category::Partial< T >
	The Kleisli Context for "Consistently Broken" Species. More...
struct	dedekind::category::TernaryResult< T >
	A Logic-Aware Result container for Ternary outcomes. More...
struct	dedekind::category::SafeAddTransform< T >
	Addition with overflow check (Classical Logic). More...
struct	dedekind::category::BoundedAddTransform< T, BoundaryPolicy >
	Addition that consults a user-supplied numeric boundary policy. More...
struct	dedekind::category::BoundedMulTransform< T, BoundaryPolicy >
	Multiplication with user-supplied numeric boundary policy. More...
struct	dedekind::category::BoundedDivTransform< T, BoundaryPolicy >
	Division with user-supplied numeric boundary policy. More...
struct	dedekind::category::HonestDivTransform< T >
	Division with truncation-awareness (Ternary Logic). More...
struct	dedekind::category::is_monadic< T, η_t, μ_t >
	T : C -> C with η : Id ⟹ T and μ : T² ⟹ T. More...
struct	dedekind::category::is_comonadic< W, ε_t, δ_t >
	Trait: the comonad laws for ε and δ on W, the duals. More...
struct	dedekind::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. More...
struct	dedekind::category::Boole
	The internal logic of the Classical Topos ({True, False}). More...
struct	dedekind::category::Kleene
	The internal logic of the Kleene Topos. More...
struct	dedekind::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. More...
struct	dedekind::category::Percentage
	Percentage: a range-enforcing [0,100] carrier ("50:50"). More...
struct	dedekind::category::Percent
	The bounded confidence chain: a 101-grade De Morgan (Kleene) chain, self-dual about 50. More...
struct	dedekind::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. More...
struct	dedekind::category::GetLogic< Ternary >
struct	dedekind::category::GetLogic< T >
struct	dedekind::category::ClassifierLogic< T >
	The logic species a classifier answer type belongs to. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::Semidecided
	The 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. More...
class	dedekind::category::Truth< L >
	The Monic Wrapper for a Logical Species (Ω). More...
struct	dedekind::category::SpeciesTraits< Truth< L > >
	Bridge the Monic Wrapper to the Logic Species Registry. More...
struct	dedekind::category::LogicTraits< T >
	Primary Template: Default to Classical (Boolean) Logic. More...
struct	dedekind::category::SubobjectClassifier< T >
struct	dedekind::category::NegationArrow< L >
	The arrow reading of logic negation ¬ = L::RFL on the truth object Ω — the canonical order-reversing arrow. More...
struct	dedekind::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). More...
struct	dedekind::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. More...
struct	dedekind::category::RunCombine
	The 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. More...
struct	dedekind::category::is_symmetric< T, Rel >
	Engineer-supplied trait: relation Rel on T is symmetric (∀x, y: Rel(x, y) ⇔ Rel(y, x)). More...
struct	dedekind::category::is_equality< T, Rel >
	Trait: Rel on T is equality, the diagonal Δ: Rel(a, b) holds iff a and b are the same value. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::Windows
	windows(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. More...
struct	dedekind::category::LastOf< T >
	The history comonad's counit: a prefix's last letter. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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). More...
struct	dedekind::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). More...
struct	dedekind::category::antitone_on_even_lengths< Rank >
	A rank whose values do not grow along the even lengths, so that ranking the even lengths descending reads them upwards. Derived, not registered per rank: a family's occurrences in the words of length N are \((N - n + 1)\) offsets times its density times \(|\Sigma|^N\), a product of non-negative sequences that do not grow, which does not grow either. The product law, stated here for the join's exact count; a general one belongs in :posetal, on an exact carrier or on an extent, since a word's × wraps and an antitone product past it is not antitone (#1134). More...
struct	dedekind::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. More...
struct	dedekind::category::Take< K >
	take<K>(), SQL's LIMIT: the first K present elements. More...
struct	dedekind::category::is_involutive< F, T >
	Trait: a callable F is involutive on T iff F(F(x)) = x for all x ∈ T. Primary is std::false_type; opt-in via specialisation or member discovery (mirrors :species's is_reflexive / is_transitive export pattern). It is the CERTIFICATE the shape cannot supply: F² = Id is a claim about F, not a syntactic property of its call. More...
struct	dedekind::category::Reverse
	An 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. More...
struct	dedekind::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>. More...
struct	dedekind::category::unit_witness< maybe_functor< T >, T >
struct	dedekind::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). More...
struct	dedekind::category::unit_witness< tuple_functor< T >, T >
struct	dedekind::category::counit_witness< tuple_functor< T >, T >
struct	dedekind::category::is_kleisli_triple< Functor >
	Trait: Functor's unit and bind satisfy the Kleisli-triple laws (Manes): \(\eta(x)^* f = f(x)\), \(m^* \eta = m\) and \((m^* f)^* g = m^* (x \mapsto f(x)^* g)\). A certificate, primary false, declared where a container's bind keeps them by construction. More...
struct	dedekind::category::is_cokleisli_triple< Functor >
	Trait: the co-Kleisli-triple laws, the duals, for Functor's counit and extend. More...
struct	dedekind::category::is_frobenius_monad< Functor >
	Trait: Functor's multiplication and comultiplication satisfy the Frobenius law (Street, "Frobenius monads and pseudomonoids", 2004): \(T\mu \circ \delta T = \delta \circ \mu = \mu T \circ T\delta\). A certificate, primary false. Being a monad and a comonad is not enough: on streams (the diagonal monad, the suffix comonad) \(\delta \circ \mu\) reads \(s_{i+j}(i+j)\) where \(T\mu \circ \delta T\) reads \(s_{i+j}(j)\). More...
struct	dedekind::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)\). More...
struct	dedekind::category::detail_f_algebra::component_orders< Op >
	The component orders of a product order, where Op is one. More...
struct	dedekind::category::detail_f_algebra::component_orders< ProductLeq< LA, LB > >
struct	dedekind::category::BetaReduction
	The β-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. More...
struct	dedekind::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). More...
struct	dedekind::category::NumericWitness< T >
	A typed witness of numeric classification in Ω_K3. More...
struct	dedekind::category::IntervalBoundaryPolicy< T >
	Closed interval policy [lower, upper] for integral species. More...
struct	dedekind::category::FullMachineBoundaryPolicy< T >
	Full-machine boundary policy (no clipping). More...
struct	dedekind::category::NaNHolePolicy< T >
	IEEE-754 NaN-hole classifier policy for floating species. More...
struct	dedekind::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. More...
struct	dedekind::category::LatticeTop< T, Rel >
	The abstract top of the lattice over (T, Rel), dually. More...
struct	dedekind::category::Meet< A, B >
struct	dedekind::category::Join< A, B >
struct	dedekind::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. More...
struct	dedekind::category::Meet< A, B >
struct	dedekind::category::Join< A, B >
struct	dedekind::category::Not< A >
struct	dedekind::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. More...
struct	dedekind::category::over_nodes< Leaf, T >
	A property of a term's leaves, lifted over the lattice's nodes: a Meet or Join has it where both operands do and share a domain, a Not where its operand does. One rule for every carrier that lifts a leaf property over the nodes: the opt-in to | and & below, and the set objects of sets (is_set_object). More...
struct	dedekind::category::builds_lattice_nodes< T >
	A carrier's opt-in: its predicates' | and & are the lattice's nodes. False by default; a node over two that build does, where they share a domain, by over_nodes, the rule sets' is_set_object follows too. A carrier that opts in keeps the lazy | and &; the set grammar of sets takes the rest, so a type that is both, a Subobject, is the lattice's. This is the lazy form: the node is the result, for intensional and symbolic predicates. A carrier with a normal form reduces at once instead (run lists in :runs, the set grammar in sets); where the lazy and the strict forms meet is not yet uniform (#1138). More...
struct	dedekind::category::MakeMeet
	The pairing factory for the meet (∧, pullback): ⟨-,-⟩ : A×B→Meet. More...
struct	dedekind::category::MakeJoin
	The pairing factory for the join (∨, pushout): ⟨-,-⟩ : A×B→Join. More...
struct	dedekind::category::law_inactive
	Sentinel: a law that does not fire on the given node. More...
struct	dedekind::category::canonical_order
	The 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. More...
struct	dedekind::category::is_lattice_bottom_for< X, Ord >
	Is X the registered bottom of the lattice whose order is Ord? More...
struct	dedekind::category::is_lattice_bottom_for< LatticeBottom< T, Rel >, Ord >
struct	dedekind::category::is_lattice_top_for< X, Ord >
	Is X the registered top of the lattice whose order is Ord? More...
struct	dedekind::category::is_lattice_top_for< LatticeTop< T, Rel >, Ord >
struct	dedekind::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). More...
struct	dedekind::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. More...
struct	dedekind::category::carrier_of< Meet< A, B > >
struct	dedekind::category::carrier_of< Join< A, B > >
struct	dedekind::category::carrier_of< Not< A > >
struct	dedekind::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). More...
struct	dedekind::category::codomain_of< X >
struct	dedekind::category::codomain_of< Meet< A, B > >
struct	dedekind::category::codomain_of< Join< A, B > >
struct	dedekind::category::codomain_of< Not< A > >
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::is_complement< Not, T, Rel, Join, Meet >
	Opt-in trait: Not is the complement morphism for the Boolean lattice over (T, Rel, Join, Meet). The trait is the semantic gate for IsBooleanLatticeCategory — the structural side (Heyting + involutiveness of Not) is already enforced by the upstream concepts, but the complement laws. More...
struct	dedekind::category::Columns
	The 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. More...
struct	dedekind::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. More...
struct	dedekind::category::Prefix
	prefix("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. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::ReflectedWindows< R, N >
	r >> s for a section fixed by reversal and the alphabet's reflection: the same query, kept beside what it was built from, for count below to read the law from. More...
struct	dedekind::category::IsoRetract< F >
	The retract of an IsIsomorphism: its total inverse arrow wrapped in an always-engaged std::optional. More...
struct	dedekind::category::archetype< C >
	The representative presentation of an object: itself for a value type; the one it names (C::archetype) otherwise. More...
struct	dedekind::category::Morphism< A, B, Func >
	The formal structure of an Arrow f: A -> B. More...
struct	dedekind::category::Rule< A, B >
	A type-erased Morphism A -> B between Species. More...
struct	dedekind::category::Identity< T >
	The Identity Morphism and Functorial Witness. More...
struct	dedekind::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. More...
struct	dedekind::category::has_one_value< T >
	Trait: the type T has exactly one value, so that two of its values are equal without comparing them: an empty type, or a composite of two such, whose legs leave nothing to choose. What lets a law read on a type speak of the one value it has (:natural). More...
struct	dedekind::category::commutes< F, G >
	Trait: the arrows F and G commute, \(f \circ g = g \circ f\): a certificate, primary std::false_type, since that two particular maps commute is a claim about them, not a property of their calls, and composition commutes for no category in general. Read symmetrically by commutes_v. It is a naturality square with one functor (:natural), and what makes a composite of two involutions one (:involution, :posetal). More...
struct	dedekind::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. More...
struct	dedekind::category::operations::compose
struct	dedekind::category::is_self_inverse< F >
	Hook: an arrow that is its own inverse ( \(f \circ f = \mathrm{id}\)). Declared here, with the inverse it licenses, ahead of IsIsomorphism, so that concept finds the inverse by ordinary lookup for an arrow in any namespace, not only through argument-dependent lookup. :involution sets it for every certified involution. More...
struct	dedekind::category::is_homomorphism< F, T, Op, Op2 >
	The homomorphism law of a map F on the carrier T, declared: \(f(a \odot b) = f(a) \circledast f(b)\), Op on T and Op2 on the codomain, a homomorphism of magmas (Bourbaki, Algebra I, §I.1.1); for a unary operation, \(f(u(a)) = u'(f(a))\). A certificate, false where none is declared: the law is an equation on every pair, so it is declared and witnessed by computation at the declaration, as is_monic_arrow_v. A class template, so that a family of maps declares it once across modules; keyed like is_involutive<F, T>, a bare callable naming its carrier. More...
struct	dedekind::category::Subobject< A, Chi >
	The Subobject Species S ↣ A. More...
struct	dedekind::category::is_reflexive< T, Rel >
	Trait to mark a relation as reflexive: a ~ a = True. More...
struct	dedekind::category::is_transitive< T, Rel >
struct	dedekind::category::is_antisymmetric< T, Rel >
struct	dedekind::category::is_connex< T, Rel >
struct	dedekind::category::Sup
	Value-returning chain lattice ops — the honest T × T → T meet / join. More...
struct	dedekind::category::Inf
	Meet ∧: the greatest lower bound on a chain (min), returned by value. Value-returning sibling of Sup. More...
struct	dedekind::category::SpeciesTraits< T, Args >
struct	dedekind::category::is_associative< T, Op >
	Trait to mark an operation as associative: (a ∘ b) ∘ c = a ∘ (b ∘ c). More...
struct	dedekind::category::is_commutative< T, Op >
	Trait to mark an operation as commutative: a ∘ b = b ∘ a. More...
struct	dedekind::category::is_idempotent< T, Op >
	Trait to mark an operation as idempotent: a ∘ a = a. More...
struct	dedekind::category::unit_trait< T, Op, typename >
struct	dedekind::category::inverse_trait< T, Op >
	The Formal Trait: Hooks the bridge into the Concept system. More...
struct	dedekind::category::is_transfinite< T >
	Primary trait for Transfiniteness. More...
struct	dedekind::category::origin_trait< T >
	Primary trait: The distinguished 'Point' of a species. More...
struct	dedekind::category::monotone_trait< F, Op >
	User-declared monotonicity witness for an arrow type F with respect to the ambient order relation Op. More...
struct	dedekind::category::antimonotone_trait< F, Op >
	User-declared anti-monotonicity witness for an arrow type F with respect to the ambient order relation Op. More...
struct	dedekind::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). More...
struct	dedekind::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. More...
struct	dedekind::category::ImageChi< F >
	The characteristic predicate of image_of(F) — recognises y as "in the image of @c F". More...
struct	dedekind::category::ImageChi< F >
	Image classifier for a retractable arrow: y is in the image iff the retract fires at y. More...
struct	dedekind::category::kernel_quotient< F >
	Opt-in trait: textbook claim "for this @c F, @c A/ker(F) is the carrier @c ::Class". More...
struct	dedekind::category::image_carrier< F >
	Opt-in trait: textbook claim "for this @c F, @c im(F) is the carrier @c ::type". More...
struct	dedekind::category::adjunction_witness< Left, Right, Unit, Counit >
	Typed unit/counit data for an adjunction witness. More...
struct	dedekind::category::is_adjoint< F, G, Op >
	The adjunction law \(f(x) \le y \iff x \le g(y)\) as an opt-in leaf fact, with the one theorem derived here: a monotone isomorphism is adjoint to its inverse ( \(f(x) \le y \iff x \le f^{-1}(y)\), both legs monotone). Other adjunctions register their fact where their theorem is stated (Δ ⊣ ∧ per glb in :cartesian_bicategory, S ⊣ P on the saturating ℤ in numbers:integer, the antitone involution's self-adjunction in algebra:ordered_algebra). More...
struct	dedekind::category::is_linear_action< M, S, AddM, AddS, MultS, Act >
	The semimodule laws of an action Act : S x M -> M, declared: 1 m = m, 0 m = 0, (s + t) m = s m + t m, (s t) m = s (t m) and s (m + n) = s m + s n. A certificate, false where none is declared: a carrier with the right signatures is not thereby a semimodule. For scalars of type size_t, the integers modulo 2^64, the laws make n m the n-fold sum of m for every n. More...
struct	dedekind::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. More...
struct	dedekind::category::ZeroAction< A, B, Op >
	The 'Absorption' logic. More...
struct	dedekind::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. More...
struct	dedekind::category::is_integer_chain< T >
	Whether a carrier is an integer chain: the integral types, and the carriers that register themselves (sets' cardinals, a bignum). More...
class	dedekind::category::unfold_view< S, Coalg >
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::Unfold< S, Coalg >
	The anamorphism of a coalgebra as an arrow from the seeds: x >> unfold<S>(c) is unfold(x, c). More...
struct	dedekind::category::Mapped< S, Coalg, F >
	The functor's action on a coalgebra: f on the emitted leg. More...
class	dedekind::category::chain_view< C >
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::category::Curried< T, Op >
	\(T \to T^T\): the operation, one argument at a time. More...
struct	dedekind::category::Uncurried< T, Op >
	\(T \times T \to U\): the curried operation, taken back. More...
struct	dedekind::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). More...
struct	dedekind::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). More...
struct	dedekind::category::Sections< T, Op >
struct	dedekind::category::Morphisms< T, Op >
struct	dedekind::category::Arrows< T, Op >
struct	dedekind::category::arrow_as_relation< F >
	Adapter: realise an IsArrow F : A → B as a binary relation (a, b) ↦ f(a) == b. More...
struct	dedekind::category::Pairing< F, G >
	⟨f, g⟩ : A → B × C, one argument into a product. More...
struct	dedekind::category::Copairing< F, G >
	[f, g] : A + B → C, case analysis out of a sum. More...
struct	dedekind::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. More...
struct	dedekind::category::Delete< A >
	Delete (counit) ε:A→1. Completes the commutative comonoid. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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. More...
struct	dedekind::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). More...
struct	dedekind::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. More...
struct	dedekind::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. More...

Enumerations
enum class	dedekind::category::Ternary : std::int8_t { False = -1 , Unknown = 0 , True = 1 }
	A three-valued propositional logic for handling partial information. More...
enum class	dedekind::category::CardinalityTag { Finite , Countable , Continuum }
enum class	dedekind::category::Holes : bool { break_match , skip }
	What a byte outside the alphabet does to a match: break it, the matcher back at its start (no word of the set holds the byte), or be skipped, the matcher as it was. Never a match itself.
enum class	dedekind::category::ArrowLaw : unsigned {   Injective , Surjective , Monotone , Antitone ,   Involutive , Constant }
enum class	dedekind::category::ArrowNode {   Compose , Product , Sum , Pairing ,   Copairing }
	The formers of arrows: g ∘ f, f × g, f + g, ⟨f, g⟩, [f, g].

Typedefs
template<typename T>
using	dedekind::category::Maybe = std::optional<T>
	The Maybe endofunctor T, implemented via std::optional.
using	dedekind::category::One = std::monostate
	The Terminal Object (1): the unique sink of every morphism.
using	dedekind::category::Zero = std::nullptr_t
	The Initial Object (0): the unique source of every morphism.
template<std::size_t K>
using	dedekind::category::At = std::integral_constant<std::size_t, K>
	The projections π_k out of a product, one family: π_1, π_2 (Pierce, Basic Category Theory for Computer Scientists §1.4), π_3 and π_<k> for a flat n-ary product, and π for the one-fold product A¹ ≅ A, whose projection is the identity.
template<std::size_t K, typename P>
using	dedekind::category::Π = typename detail_limit::projection_arrow<K, P>::type
	π_k read at the product P, as a MORPHISM (Domain = P, Codomain the k-th part): the building block of IsArrowProduct. Π<0, P> is Identity
using	dedekind::category::TerminalCategory = DiscreteCategory<One>
using	dedekind::category::InitialCategory = DiscreteCategory<Zero>
using	dedekind::category::Alphabet
	The byte alphabet's type, as abc builds it: the letters under their predicate, a filtered chain of the bytes. Listing 5's Alphabet bases. (#1141: the first carrier of the alphabet concept.).
using	dedekind::category::Words = Powers<std::byte, Letters, std::size_t>
	The words over the byte alphabet, by length: words(Σ)'s type, Listing 5's Words oligos.
template<std::size_t Bits>
using	dedekind::category::narrowest_count_word
	The narrowest count word on the ladder holding Bits: the stage of the filtered colimit a count of that many bits factors through. The rungs are the words whose products stay in them (IsCountWord): 32 and 64 bits; past the top there is none, and the count stays in its factors, compared and multiplied exactly there.
template<std::size_t W>
using	dedekind::category::BitWord = typename detail_periodic::bit_word<W>::type
	The bit word of width W, chosen by the width: the machine word for 8, 16, 32 and 64 bits, std::bitset otherwise.
template<typename Less>
using	dedekind::category::lattice_less_logic_t = typename lattice_less_logic<Less>::type
template<typename Term, typename Less, typename Ord = canonical_order, typename Combine = no_leaf_combine>
using	dedekind::category::reduce_t
	The normal form of Term under Reduce<Less, Ord, Combine>: the type the fold produces, read without running it.
template<typename C>
using	dedekind::category::disc_self_endofunctor_t = identity_functor<C>
	Discrete-restriction representative of the textbook Disc / U functor: the identity endofunctor on a discrete category C.
template<typename C>
using	dedekind::category::disc_self_unit_t = identity_transformation<disc_self_endofunctor_t<C>>
	Discrete-restriction representative of the textbook unit η / counit ε of the Disc ⊣ U adjunction: the identity natural transformation on disc_self_endofunctor_t<C>.
template<typename X, typename Y = X>
using	dedekind::category::Constant = ConstantMorphism<X, Y>
	The constant arrow by its short name, the paper's spelling.
template<typename Pred, typename T>
using	dedekind::category::OmegaOf
	Extract the Ω-type of a LogicalMap.
template<typename T>
using	dedekind::category::classifier_logic_t
template<typename L1, typename L2>
using	dedekind::category::join_logic_t = typename join_logic<L1, L2>::type
template<typename L1, typename L2>
using	dedekind::category::meet_logic_t = typename meet_logic<L1, L2>::type
template<typename T>
using	dedekind::category::LogicOf = typename LogicTraits<T>::type
	Shorthand for the Logic Species of a type.
template<typename T>
using	dedekind::category::Omega = typename LogicOf<T>::Ω
	Shorthand for the Subobject Classifier (Omega) of a species.
using	dedekind::category::ascending = std::less<>
	The orders a query is sorted by, the standard's comparisons named as SQL's ASC and DESC: the defaults of order_by's parameter, which takes any comparison with sufficient structure, a total preorder on the rank's values.
using	dedekind::category::descending = std::greater<>
template<std::semiregular Op>
using	dedekind::category::Opposite = typename detail_involution::opposite<Op>::type
	The opposite operation, \(a \cdot^{op} b = b \cdot a\), the product of the opposite monoid \(M^{op}\) (Mac Lane, Categories for the Working Mathematician, II.2), an involution on operations: Opposite<Opposite<Op>> is Op, the same type. A left action of \(M\) is a right action of \(M^{op}\), so a left action folded along a walk acts by the product in \(M^{op}\). The laws read backwards are the laws: associativity, the unit, commutativity and idempotence carry over, declared once here, and totality in :total.
template<typename MA>
using	dedekind::category::functor_of_t = typename functor_of<std::remove_cvref_t<MA>>::type
using	first = LA
using	second = LB
template<typename P>
using	dedekind::category::predicate_logic_t = typename predicate_logic<P>::type
template<typename T, typename Ord>
using	dedekind::category::resolved_order_t
	The comparator Ord resolves to for a carrier T: std::less_equal<T> for canonical_order, otherwise Ord itself.
template<typename X>
using	dedekind::category::carrier_of_t = typename carrier_of<X>::type
template<typename X>
using	dedekind::category::codomain_of_t = typename codomain_of<X>::type
template<typename C>
using	dedekind::category::archetype_t = typename archetype<C>::type
template<IsArrow F>
using	dedekind::category::Dom = typename std::remove_cvref_t<F>::Domain
	Shorthand to look up the Domain of an Arrow type F.
template<IsArrow F>
using	dedekind::category::Cod = typename std::remove_cvref_t<F>::Codomain
	Shorthand to look up the Codomain of an Arrow type F.
template<typename A, typename L = Boole>
using	dedekind::category::PowerObject = Exponential<A, typename L::Ω>
	Power Object Alias.
using	dedekind::category::ArrowLaws = Profile<ArrowLaw, every_arrow_law.size()>
	The profile of a function.
template<std::regular X, std::semiregular Step>
using	dedekind::category::chain_t = unfold_view<X, StepCoalgebra<X, Step>>
	The chain of x under a partial step: what the step reaches from x, the step of it, then the step of that, until the step has nothing (Dedekind's chain of the step of x, [4]). With Prior it is \(n - 1, \ldots, 0\), the n elements below n, n itself excluded: the Jlt paper's Figure 2, after Lambek.
template<IsCountWord N, IsFiniteChainSequence F>
using	dedekind::category::FiniteChainSequence
	The finite sequence as a value, n >> chain<N>() >> f: the chain of n read by f, never built. A fold over it is the list as its fold, the Church encoding (#1133).
template<typename A, typename B>
using	dedekind::category::Exponential
	The Exponential Object B^A (Type Alias).
template<std::size_t K, typename A, typename B>
using	dedekind::category::ι = Injection<K, A, B>
	The injection by its textbook name, \(\iota_K\) (Pierce), as the projection is Π.
template<typename A>
using	dedekind::category::CanonicalSetCCC = Set<A>
	Explicit alias for the canonical ETCS CCC witness over ambient A.
template<IsArrow F, IsArrow G>
using	dedekind::category::ProductArrow
	f × g = ⟨f ∘ π₁, g ∘ π₂⟩ : A × C → B × D.
template<typename A, typename B>
using	dedekind::category::Flip = Pairing<Π<2, std::pair<A, B>>, Π<1, std::pair<A, B>>>
	flip, the symmetry of the cartesian product, \(\sigma_{A,B} : A \times B \to B \times A\): the pairing of the projections the other way round, \(\langle \pi_2, \pi_1 \rangle\). On a square an involution, so an isomorphism, its own inverse; natural in both factors, \(\sigma \circ (f \times g) = (g \times f) \circ \sigma\), the braiding of the cartesian monoidal structure, symmetric. A word of two letters flipped is the word reversed.
template<IsArrow F, IsArrow G>
using	dedekind::category::SumArrow
	f + g = [ι₁ ∘ f, ι₂ ∘ g] : A + C → B + D.
template<typename S>
using	dedekind::category::discrete_lift_t = DiscreteCategory<S>

Functions
template<std::integral T>
constexpr T	dedekind::category::successor (T n) noexcept
	The successor arrow as a free customization point: successor(n) for an NNO carrier, and its partial dual predecessor(n).
template<std::integral T>
constexpr T	dedekind::category::predecessor (T n) noexcept
template<typename T> requires requires(const T& n) { { T::successor(n) } -> std::convertible_to<T>; }
constexpr T	dedekind::category::successor (const T &n)
	Bridge to the :morphologies static-member convention.
constexpr bool	dedekind::category::predecessor (bool) noexcept
constexpr std::byte	dedekind::category::successor (std::byte b) noexcept
	The octets' covering step: std::byte's order read as a chain, the next byte, saturating at the top. No arithmetic, only the step, so a byte chain is a chain and no integer chain.
constexpr std::byte	dedekind::category::predecessor (std::byte b) noexcept
template<HasNNOStep N> requires std::equality_comparable<N>
constexpr std::optional< N >	dedekind::category::cover (const N &n)
	The cover \(S^{+} : N \to 1 + N\) (y covers x: x < y, nothing between, Davey and Priestley [3], ch. 1): the successor read partially, nullopt at a fixpoint of S, which on a saturating bounded chain is its top (ℵ₀ on Cardinality, True on K₃), and at a machine word's greatest value, where S has no value (signed) or wraps (unsigned: the ring ℤ/2^w under S, the chain 0 < 1 < … < 2^w − 1 under its cover); total on an unbounded chain. Whether the step itself is monotone is the arrow's fact (IsMonotone<Successor<N>>, registered in order:completeness from the carrier's periodicity), not the carrier's. std::optional<N> is \(1 + N\), the NNO's own functor \(F(X) = 1 + X\).
template<HasNNOStep N> requires std::equality_comparable<N>
constexpr std::optional< N >	dedekind::category::lower_cover (const N &n)
	The lower cover \(P^{+} : N \to 1 + N\), dual to cover: the predecessor read partially, nullopt at the least element (a fixpoint of P, or a machine word's least value). Not the destructor Prior, which is nothing at zero.
template<typename A, typename G> requires std::regular_invocable<const G&, const A&> && std::convertible_to<std::invoke_result_t<const G&, const A&>, A> && std::copyable<A>
constexpr A	dedekind::category::nno_iterate (A a0, G g, std::size_t n)
	Recursion-via-universal-property (operational discharge).
template<typename 𝗙, typename 𝗚> requires IsArrow<std::decay_t<𝗙>> && IsArrow<std::decay_t<𝗚>> && std::same_as<typename std::decay_t<𝗙>::Codomain, typename std::decay_t<𝗚>::Domain> && IsShapedFunctor<𝗙> && IsShapedFunctor<𝗚> && std::same_as<typename std::remove_cvref_t<𝗙>::Τ_cat, typename std::remove_cvref_t<𝗚>::Σ_cat>
constexpr auto	dedekind::category::operator>> (𝗙 f, 𝗚 g)
template<typename 𝗙, typename 𝗚> requires IsArrow<std::decay_t<𝗙>> && IsArrow<std::decay_t<𝗚>> && std::same_as<typename std::decay_t<𝗙>::Codomain, typename std::decay_t<𝗚>::Domain> && IsShapedFunctor<𝗙> && IsShapedFunctor<𝗚> && std::same_as<typename std::remove_cvref_t<𝗙>::Τ_cat, typename std::remove_cvref_t<𝗚>::Σ_cat> && IsIdentityFunctor<𝗙>
constexpr auto	dedekind::category::operator>> (𝗙, 𝗚 g)
template<typename 𝗙, typename 𝗚> requires IsArrow<std::decay_t<𝗙>> && IsArrow<std::decay_t<𝗚>> && std::same_as<typename std::decay_t<𝗙>::Codomain, typename std::decay_t<𝗚>::Domain> && IsShapedFunctor<𝗙> && IsShapedFunctor<𝗚> && std::same_as<typename std::remove_cvref_t<𝗙>::Τ_cat, typename std::remove_cvref_t<𝗚>::Σ_cat> && IsIdentityFunctor<𝗚>
constexpr auto	dedekind::category::operator>> (𝗙 f, 𝗚)
template<typename 𝗙, typename 𝗚> requires IsArrow<std::decay_t<𝗙>> && IsArrow<std::decay_t<𝗚>> && std::same_as<typename std::decay_t<𝗙>::Codomain, typename std::decay_t<𝗚>::Domain> && IsShapedFunctor<𝗙> && IsShapedFunctor<𝗚> && std::same_as<typename std::remove_cvref_t<𝗙>::Τ_cat, typename std::remove_cvref_t<𝗚>::Σ_cat> && IsIdentityFunctor<𝗙> && IsIdentityFunctor<𝗚>
constexpr auto	dedekind::category::operator>> (𝗙 f, 𝗚)
template<typename 𝗙, typename 𝗚> requires IsShapedFunctor<𝗙> && IsShapedFunctor<𝗚> && std::same_as<typename std::remove_cvref_t<𝗚>::Τ_cat, typename std::remove_cvref_t<𝗙>::Σ_cat>
constexpr auto	dedekind::category::operator<< (𝗙 f, 𝗚 g)
	The "Upstream Fish" (Optional Composition Sugar) g << f => g ∘ f.
template<typename Functor, typename Structure> requires IsEndofunctor<std::remove_cvref_t<Functor>> && IsArrow<std::remove_cvref_t<Structure>>
constexpr auto	dedekind::category::make_f_algebra (Functor functor, Structure structure)
	Factory for F-algebra witnesses.
template<typename Functor, typename Structure> requires IsEndofunctor<std::remove_cvref_t<Functor>> && IsArrow<std::remove_cvref_t<Structure>>
constexpr auto	dedekind::category::make_f_coalgebra (Functor functor, Structure structure)
	Factory for F-coalgebra witnesses.
template<typename T, typename Step, typename Equal = std::equal_to<>> requires IsIterativeEndomorphism<T, Step> && std::predicate<const Equal&, const T&, const T&>
constexpr T	dedekind::category::fixed_point (T seed, Step step, Equal equal={}, std::size_t max_iterations=1024)
	Iteratively compute a fixed point of an endomorphism.
template<typename T, typename Step, typename Equal = std::equal_to<>> requires IsIterativeEndomorphism<T, Step> && std::predicate<const Equal&, const T&, const T&>
constexpr T	dedekind::category::least_fixpoint (T seed, Step step, Equal equal={}, std::size_t max_iterations=1024)
	Alias emphasizing order-theoretic reading of the fixed point.
template<typename T, typename Expand, typename Join, typename Equal = std::equal_to<>> requires std::predicate<const Equal&, const T&, const T&>
constexpr T	dedekind::category::closure (const T &x, Expand expand, Join join, Equal equal={}, std::size_t max_iterations=1024)
	The closure of x under expand: the textbook "closure of @c X under @c Y". It is the least fixpoint of S ↦ x ⊔ expand(S) — the smallest element ⊒ x closed under the one-step expansion expand — equivalently the Kleene join ⨆ₙ expandⁿ(x).
template<typename A, typename B, typename Op = std::plus<B>> requires IsPointed<B, Op>
constexpr auto	dedekind::category::zero ()
	zero<A, B, Op>(): the constant morphism A → B that maps everything to the Op-identity element of B. Defaults to std::plus (additive identity, i.e. zero); with std::multiplies it is the constant at one.
template<std::ranges::input_range R, typename T = std::ranges::range_value_t<R>, typename Op = std::plus<T>> requires IsMonoid<T, Op>
constexpr T	dedekind::category::concat (R r, Op op={})
	The free monoid's fold, concat, the canonical fold of a monoid: a range folded under the operation from its unit (the Jlt paper's Listings 2 to 4). Its specialisation, licensed by associativity, folds n copies of one value, any IsCopies range, by the binary method, one squaring per bit of n (Knuth, TAOCP 2 §4.6.3). Resolution picks it over the plain fold, its parameter being the more specific.
template<IsCountWord N, IsConstantArrow F>
constexpr N	dedekind::category::copies_count (const unfold_view< N, Mapped< N, StepCoalgebra< N, Prior< N > >, F > > &r)
	The counting chain of n under a constant arrow, n >> chain<N>() >> constant(x), is n copies of x, counted in the chain's own word.
template<IsCountWord N, IsConstantArrow F>
constexpr Cod< F >	dedekind::category::copies_value (const unfold_view< N, Mapped< N, StepCoalgebra< N, Prior< N > >, F > > &r)
template<std::copy_constructible T, std::integral B> requires (!std::same_as<B, bool>)
constexpr std::make_unsigned_t< B >	dedekind::category::copies_count (const std::ranges::repeat_view< T, B > &r)
	The standard's views::repeat(x, n) is n copies of x; its value is read only where n is not zero.
template<std::copy_constructible T, std::integral B> requires (!std::same_as<B, bool>)
constexpr T	dedekind::category::copies_value (const std::ranges::repeat_view< T, B > &r)
template<std::ranges::input_range R, typename T = std::ranges::range_value_t<R>, typename Op = std::plus<T>> requires IsMonoid<T, Op> && IsCopies<R>
constexpr T	dedekind::category::concat (R r, Op op={})
	concat on n copies of one value: its n-th power, by squaring its first half, licensed by associativity. The same signature as the plain fold and a stronger constraint, so resolution prefers it wherever IsCopies holds. The value is read only where there is a copy, as a model promises it.
template<typename T>
constexpr auto	dedekind::category::bang ()
	The terminal map factory: produces the unique arrow !: T → One.
template<typename T>
constexpr auto	dedekind::category::zero ()
	The zero morphism factory: produces the unique (unreachable) arrow ?: Zero → T.
template<typename P, std::size_t K> requires TupleLike<P> && (K >= 1) && (K <= std::tuple_size_v<P>)
constexpr auto	dedekind::category::component (const P &p, At< K >)
	The k-th component of a tuple-like product, by reference: a projection reads its point without copying it (a string or vector carrier stays where it is). π_k returns a temporary's component by value.
template<typename P> requires (!TupleLike<P>) && requires(const P& p) { p.first; }
constexpr auto	dedekind::category::component (const P &p, At< 1 >)
	The components of a pair-like product that is not tuple-like.
template<typename P> requires (!TupleLike<P>) && requires(const P& p) { p.second; }
constexpr auto	dedekind::category::component (const P &p, At< 2 >)
template<IsArrow F, IsArrow G> requires std::same_as<Dom<F>, Dom<G>>
constexpr auto	dedekind::category::mediate_product (F f, G g)
	Mediating morphism for Products: ⟨f, g⟩: X -> (A × B).
template<typename S> requires IsSubobject<S, typename S::Domain>
constexpr auto	dedekind::category::in (const typename S::Domain &x, const S &s)
	Membership: x ∈ S evaluated via S's structural call (the carrier IS the characteristic morphism).
template<typename S, IsArrow E> requires IsSubobject<S, typename S::Domain> && std::same_as<Cod<E>, typename S::Domain>
constexpr auto	dedekind::category::in_via (const Dom< E > &x, E embedding, const S &s)
	Membership through an embedding arrow e:X→A, then the carrier-as-predicate: x ∈_e S = s(e(x)).
template<IsArrow F, IsArrow G> requires std::same_as<Cod<std::decay_t<F>>, Dom<std::decay_t<G>>>
constexpr auto	dedekind::category::compose_embedding (F f, G g)
	Compose two embedding arrows for pullback naturality path checks.
template<HasPeriod F, IsArrow G>
constexpr Dom< F >	dedekind::category::period (const Compose< F, G > &c)
	Inferred, not declared: an arrow after a periodic one is periodic with the same period, whatever the second arrow is.
template<HasPeriod F>
constexpr Dom< F >	dedekind::category::extent (const F &)
	Where a period's law holds: \(f(k + p) = f(k)\) for every k with k + p below the extent. A generator's law holds on the whole word; a shift narrows it, since the word does not wrap for the law.
template<HasPeriod F, IsArrow G>
constexpr Dom< F >	dedekind::category::extent (const Compose< F, G > &c)
template<IsCountWord N, typename B>
constexpr N	dedekind::category::period (const ConstantMorphism< N, B > &)
	A constant sequence, a constant arrow out of the counts: period 1, on the whole word. A constant arrow from anything else is no sequence and has no period.
template<IsCountWord N>
constexpr N	dedekind::category::period (const Congruent< N > &c)
template<IsCountWord N = std::size_t>
constexpr Congruent< N >	dedekind::category::congruent (std::type_identity_t< N > m, std::type_identity_t< N > r)
	The residue class of r modulo m.
template<IsCountWord N>
constexpr N	dedekind::category::period (const FibonacciMod< N > &f)
	The Pisano period \(\pi(m)\), the period of the Fibonacci numbers modulo m, a theorem: it exists and is at most \(6m\), so a search of that length finds it.
template<IsCountWord N = std::size_t>
constexpr FibonacciMod< N >	dedekind::category::fibonacci_mod (std::type_identity_t< N > m)
	The Fibonacci numbers modulo m.
template<IsArrow F>
constexpr Opaque< F >	dedekind::category::opaque (F f)
template<IsCountWord N = std::size_t, std::ranges::input_range R> requires std::convertible_to<std::ranges::range_value_t<R>, bool>
constexpr N	dedekind::category::count (R r)
	The count of a range of truth values: the plain fold.
template<IsCountWord N, HasPeriod F> requires std::same_as<Dom<F>, N> && std::convertible_to<Cod<F>, bool>
constexpr N	dedekind::category::count (const FiniteChainSequence< N, F > &v)
	The count along the chain of n under a periodic predicate: (n div p) periods and a remainder, by periodicity; the chain's order does not matter, since the counts commute. More specialised than the plain fold, so resolution prefers it.
template<IsCountWord N, HasPeriod F> requires std::same_as<Dom<F>, N> && std::convertible_to<Cod<F>, bool>
constexpr N	dedekind::category::count (const unfold_view< std::optional< N >, detail_chain::SliceStep< N, F > > &v)
	The count along a chain restricted by value to [lo, hi) under a periodic predicate: the law's count below hi less the law's count below lo, two calls whatever the bounds.
template<std::ranges::input_range R> requires IsCountWord<std::ranges::range_value_t<R>>
constexpr std::ranges::range_value_t< R >	dedekind::category::sum (R r)
	The sum of a range of counts: the plain fold.
template<IsCountWord N, HasPeriod F> requires std::same_as<Dom<F>, N> && std::same_as<Cod<F>, N>
constexpr N	dedekind::category::sum (const FiniteChainSequence< N, F > &v)
	The sum along the chain of n under a periodic arrow into the counts: (n div p) copies of one period's sum, one multiplication by the semimodule law, and a remainder.
template<IsCountWord N, HasUnitPeriod F> requires std::same_as<Dom<F>, N> && std::same_as<Cod<F>, N>
constexpr N	dedekind::category::sum (const FiniteChainSequence< N, F > &v)
	The sum along the chain of n under a sequence of period 1 by its type, a constant one on its extent: n copies of f(0), one multiplication by the semimodule law, and no fold at all, not even over a period of one or a remainder of none. The action of \(\mathbb{N}\) on the counts collapsing a constant, as Listing 4's concat on copies does. More specialised than the periodic sum, so resolution prefers it.
template<std::ranges::input_range R> requires detail_periodic::is_exact_count_v<std::ranges::range_value_t<R>>
constexpr std::ranges::range_value_t< R >	dedekind::category::exact_sum (R r)
	The exact sum of a range of exact counts: the plain fold, never wrapped, the discipline of exact_count.
template<IsCountWord N, HasPeriod F> requires std::same_as<Dom<F>, N> && std::same_as<Cod<F>, std::optional<N>>
constexpr std::optional< N >	dedekind::category::exact_sum (const FiniteChainSequence< N, F > &v)
	The exact sum along the chain of n under a periodic arrow into the exact counts: sum's law, checked.
template<IsCountWord N, HasUnitPeriod F> requires std::same_as<Dom<F>, N> && std::same_as<Cod<F>, std::optional<N>>
constexpr std::optional< N >	dedekind::category::exact_sum (const FiniteChainSequence< N, F > &v)
	The exact sum along a constant sequence: sum's collapse, checked.
template<IsCountWord N = std::size_t>
constexpr Shift< N >	dedekind::category::shift (std::type_identity_t< N > j)
template<IsCountWord N, HasPeriod G>
constexpr N	dedekind::category::period (const Compose< Shift< N >, G > &c)
template<IsCountWord N, HasPeriod G>
constexpr N	dedekind::category::extent (const Compose< Shift< N >, G > &c)
template<HasPeriod P, HasPeriod Q>
constexpr Dom< P >	dedekind::category::period (const Join< P, Q > &j)
template<HasPeriod P, HasPeriod Q>
constexpr Dom< P >	dedekind::category::period (const Meet< P, Q > &m)
template<HasPeriod P, HasPeriod Q>
constexpr Dom< P >	dedekind::category::extent (const Join< P, Q > &j)
template<HasPeriod P, HasPeriod Q>
constexpr Dom< P >	dedekind::category::extent (const Meet< P, Q > &m)
template<HasPeriod P>
constexpr Dom< P >	dedekind::category::period (const Not< P > &n)
template<HasPeriod P>
constexpr Dom< P >	dedekind::category::extent (const Not< P > &n)
template<detail_periodic::IsPeriodicPredicate F, std::semiregular Step, std::semiregular Acc>
constexpr Dom< F >	dedekind::category::period (const Rolling< F, Step, Acc > &r)
template<detail_periodic::IsPeriodicPredicate F, std::semiregular Step, std::semiregular Acc>
constexpr Dom< F >	dedekind::category::extent (const Rolling< F, Step, Acc > &r)
template<detail_periodic::IsPeriodicPredicate F>
constexpr Rolling< F, detail_periodic::CountStep< Dom< F > >, Dom< F > >	dedekind::category::rolling_count (F f, std::type_identity_t< Dom< F > > w)
	How many of w consecutive values are true, SQL's COUNT OVER a window.
template<detail_periodic::IsPeriodicPredicate F>
constexpr Rolling< F, detail_periodic::AnyStep, bool >	dedekind::category::rolling_any (F f, std::type_identity_t< Dom< F > > w)
	Whether any of w consecutive values is true.
template<IsCountWord N, IsArrow F, IsArrow G> requires std::same_as<Cod<F>, bool> && std::same_as<Cod<G>, bool>
constexpr auto	dedekind::category::operator* (const FiniteChainSequence< N, F > &a, const FiniteChainSequence< N, G > &b)
template<IsArrow T, std::size_t K, IsCountWord N, IsArrow G> requires std::same_as<Cod<G>, bool>
constexpr auto	dedekind::category::operator* (const Box< T, K, N > &x, const FiniteChainSequence< N, G > &b)
template<IsArrow T, std::size_t K, IsCountWord N>
constexpr std::array< N, K >	dedekind::category::count_factors (const Box< T, K, N > &b)
	Each leg's count over its chain, the factors of the box's count.
template<IsArrow T, std::size_t K, IsCountWord N>
constexpr N	dedekind::category::count (const Box< T, K, N > &b)
	The count over the box, SQL's COUNT(*) over a cross join: by distributivity the product of the legs' counts, contracting the rank-one tensor against the all-ones covector on each leg. Exact beyond the word only as its factors (count_factors); this is its residue.
template<IsArrow T, std::size_t K, IsCountWord N>
constexpr N	dedekind::category::count_section (const Box< T, K, N > &b, std::type_identity_t< N > m, std::type_identity_t< N > r)
	The count over the section \(i_1 + \cdots + i_K \equiv r \pmod m\) of the box, SQL's GROUP BY a computed key: the cyclic convolution of the legs' histograms over the residues, m numbers a leg, in the counts' semiring.
constexpr Letters	dedekind::category::letters (std::string_view alphabet)
constexpr auto	dedekind::category::abc (std::string_view a)
	The alphabet of its letters alone: the least slice of the bytes that holds them, under the predicate that keeps them, slice(lo, hi) >> letters(a) with lo the least letter and hi one past the greatest.
template<std::size_t M> requires (M >= 1)
constexpr Bytes< M - 1 >	dedekind::category::bytes (const char(&s)[M])
constexpr Ranked	dedekind::category::rank (const Letters &on)
constexpr Letters	dedekind::category::letters_of (const Alphabet &alphabet)
constexpr Ranked	dedekind::category::rank (const Alphabet &alphabet)
constexpr Reflection	dedekind::category::refl (const Letters &on)
constexpr Reflection	dedekind::category::refl (const Alphabet &alphabet)
constexpr RandomLetter	dedekind::category::random_letter (const Alphabet &alphabet, std::uint64_t seed=0)
constexpr auto	dedekind::category::random_text (const Alphabet &alphabet, std::size_t length, std::uint64_t seed=0)
template<std::size_t N>
constexpr std::array< std::byte, N >	dedekind::category::random_word (const Alphabet &alphabet, std::uint64_t seed=0)
	A random word held as a value, for a law's input where a stage wants contiguous letters.
constexpr LetterMap	dedekind::category::letter_map (std::string_view from, std::string_view to)
template<IsCountWord N = std::size_t, HasNNOStep C, IsArrow F> requires std::totally_ordered<C> && std::same_as<Dom<F>, C> && std::convertible_to<Cod<F>, bool>
constexpr Power< C, F, N >	dedekind::category::power (const unfold_view< std::optional< C >, detail_chain::SliceStep< C, F > > &leg, std::type_identity_t< N > n)
template<IsArrow T> requires std::same_as<Dom<T>, Cod<T>>
constexpr PowerMap< T >	dedekind::category::power (const T &tau)
template<IsCountWord N = std::size_t>
constexpr Rotation< N >	dedekind::category::rotate (std::type_identity_t< N > d)
template<IsCountWord N>
constexpr AtMost< Cycles< N >, 2 >	dedekind::category::antitone_cycle_type (N m)
	The cycle type of a finite chain's antitone bijection. A finite chain is rigid: its one antitone bijection is its reversal, the least element to the greatest and so inward, so \(\lfloor m/2 \rfloor\) pairs and, where m is odd, the middle fixed (#1133).
template<IsCountWord N>
constexpr AtMost< Cycles< N >, 2 >	dedekind::category::cycle_type (Reverse, N n)
	The cycle type of the reversal of n positions: the antitone bijection of their chain.
template<IsCountWord N>
constexpr AtMost< Cycles< N >, 1 >	dedekind::category::cycle_type (const Rotation< N > &r, N n)
	The cycle type of a rotation of n positions by d: \(g = \gcd(n, d)\) cycles of length \(n / g\), the identity where d is a multiple of n.
template<IsCountWord N>
constexpr N	dedekind::category::position (Reverse, N n, N i)
	A permutation of positions on indices: where it sends the position i of a word of length n, the reversal to \(n - 1 - i\).
template<IsCountWord N>
constexpr N	dedekind::category::position (const Rotation< N > &r, N n, N i)
template<IsArrow T> requires std::same_as<Dom<T>, std::byte> && std::same_as<Cod<T>, std::byte>
constexpr bool	dedekind::category::is_antitone (const T &t, const Letters &on)
	Whether a letter map reverses the order of an alphabet, decided on its table: the letters as bytes are a chain, and on a chain consecutive letters suffice. A law of the value, not of the type: the Watson–Crick pairing reverses A < C < G < T because of how the one-letter codes are chosen. Where it does and the map is a bijection, its cycle type is antitone_cycle_type's.
constexpr bool	dedekind::category::is_involution (const LetterMap &t)
	Whether a letter map is an involution, decided on its table: a law of the value, the 256 bytes taken twice, as a law of a finite structure is decided.
template<IsArrow T> requires std::same_as<Dom<T>, Cod<T>>
constexpr bool	dedekind::category::is_involution (const PowerMap< T > &p)
	A map on every letter is an involution where the map on one is.
template<HasNNOStep C, IsArrow F, IsCountWord N, typename S> requires HasCycleType<S, N>
constexpr Symmetric< Power< C, F, N >, S, Identity< C > >	dedekind::category::symmetric (const Power< C, F, N > &p, S sigma)
template<HasNNOStep C, IsArrow F, IsCountWord N, typename S> requires HasCycleType<S, N>
constexpr Symmetric< Power< C, F, N >, S, Identity< C > >	dedekind::category::symmetric (const Power< C, F, N > &p, const Morphism< std::vector< C >, std::vector< C >, S > &sigma)
template<HasNNOStep C, IsArrow F, IsCountWord N, IsArrow T, typename S> requires std::same_as<Dom<T>, C> && HasCycleType<S, N>
constexpr Symmetric< Power< C, F, N >, S, T >	dedekind::category::symmetric (const Power< C, F, N > &p, const Compose< PowerMap< T >, Morphism< std::vector< C >, std::vector< C >, S > > &g)
template<HasNNOStep C, IsArrow F, IsCountWord N, IsArrow T, typename S> requires std::same_as<Dom<T>, C> && HasCycleType<S, N>
constexpr Symmetric< Power< C, F, N >, S, T >	dedekind::category::symmetric (const Power< C, F, N > &p, const Compose< Morphism< std::vector< C >, std::vector< C >, S >, PowerMap< T > > &g)
template<IsCountWord N = std::size_t, HasNNOStep C, IsArrow F> requires std::totally_ordered<C> && std::same_as<Dom<F>, C> && std::convertible_to<Cod<F>, bool>
constexpr Powers< C, F, N >	dedekind::category::words (const unfold_view< std::optional< C >, detail_chain::SliceStep< C, F > > &leg)
template<IsArrow T, typename C, typename S>
constexpr detail_periodic::FixedByStage< S, T >	dedekind::category::fixed_by (const Compose< PowerMap< T >, Morphism< std::vector< C >, std::vector< C >, S > > &g)
template<IsArrow T, typename C, typename S>
constexpr detail_periodic::FixedByStage< S, T >	dedekind::category::fixed_by (const Compose< Morphism< std::vector< C >, std::vector< C >, S >, PowerMap< T > > &g)
template<HasNNOStep C, IsArrow F, IsCountWord N, typename S, IsArrow T> requires std::same_as<Dom<T>, C> && HasCycleType<S, N>
constexpr auto	dedekind::category::operator>> (const Powers< C, F, N > &ps, const detail_periodic::FixedByStage< S, T > &st)
	The powers, then the sections each fixes: a family of sets of words by length, words(Σ) >> fixed_by(g).
template<HasNNOStep C, IsArrow F, IsCountWord N, typename S, IsArrow T> requires std::same_as<Dom<T>, C> && HasCycleType<S, N>
constexpr auto	dedekind::category::operator& (const Powers< C, F, N > &ps, const detail_periodic::FixedByStage< S, T > &st)
	words(Σ) & fixed_by(g): the words g fixes, by length, the same family spelled as Trsk spells a set under a predicate.
template<IsCountWord N = std::size_t>
constexpr Length< N >	dedekind::category::len (std::type_identity_t< N > n)
template<IsArrow Fam, IsCountWord N> requires is_graded_v<Fam> && std::same_as<Dom<Fam>, N>
constexpr Cod< Fam >	dedekind::category::operator& (const Fam &fam, Length< N > l)
template<HasNNOStep C, IsArrow F, IsCountWord N, typename S, IsArrow T> requires std::same_as<Dom<T>, C> && HasCycleType<S, N>
constexpr Symmetric< Power< C, F, N >, S, T >	dedekind::category::operator& (const Power< C, F, N > &p, const detail_periodic::FixedByStage< S, T > &st)
	power(Σ, n) & fixed_by(g): the power met with what g fixes, symmetric(power, g) spelled as Trsk spells a set under a predicate. The equalizer of g and the identity, a subobject of the power, and one the laws count: from g's cycle type, no word built.
constexpr ReflectedReverse	dedekind::category::operator~ (Reverse)
constexpr detail_periodic::FixedByReflectedReverse	dedekind::category::fixed_by (ReflectedReverse)
template<IsCountWord N>
constexpr Symmetric< Power< std::byte, Letters, N >, Reverse, Reflection >	dedekind::category::operator& (const Power< std::byte, Letters, N > &p, detail_periodic::FixedByReflectedReverse)
	power & fixed_by(~rev): the words the reverse complement fixes, the complement the power's own, refl of its letters.
template<IsCountWord N>
constexpr auto	dedekind::category::operator& (const Powers< std::byte, Letters, N > &ps, detail_periodic::FixedByReflectedReverse)
	words(Σ) & fixed_by(~rev): the same, by length.
template<HasFactors A, HasFactors B> requires std::same_as< detail_periodic::word_of_t<decltype(count_factors(std::declval<A>()))>, detail_periodic::word_of_t<decltype(count_factors(std::declval<B>()))>>
constexpr Outer< A, B >	dedekind::category::operator* (const A &a, const B &b)
template<HasFactors A, HasFactors B> requires std::same_as< detail_periodic::word_of_t<decltype(count_factors(std::declval<A>()))>, detail_periodic::word_of_t<decltype(count_factors(std::declval<B>()))>>
constexpr auto	dedekind::category::count_factors (const Outer< A, B > &o)
template<IsCountWord N = std::size_t, HasNNOStep C, IsArrow F> requires std::totally_ordered<C> && std::same_as<Dom<F>, C> && std::convertible_to<Cod<F>, bool>
constexpr FreeMonoid< C, F, N >	dedekind::category::free_monoid (const unfold_view< std::optional< C >, detail_chain::SliceStep< C, F > > &leg, std::type_identity_t< N > below)
template<typename L, IsCountWord N = detail_periodic::word_of_t<L>> requires detail_periodic::IsFactorsOf<L, N>
constexpr N	dedekind::category::count (const L &fs)
	The count of a factored tensor, modulo the word: a monoid concat under * over the factors, each a concat on copies of a popcount, by squaring. Agrees with exact_count wherever the word holds the count.
template<typename L, IsCountWord N = detail_periodic::word_of_t<L>> requires detail_periodic::IsFactorsOf<L, N>
constexpr std::optional< N >	dedekind::category::exact_count (const L &fs)
	The count of a factored tensor, exactly, or none where the word cannot hold it: never wrapped, the discipline of checked_lcm.
template<typename L, IsCountWord N = detail_periodic::word_of_t<L>> requires detail_periodic::IsFactorsOf<L, N>
constexpr std::size_t	dedekind::category::bits_needed (const L &fs)
	The bits a count needs at most, read off its factors without multiplying them: \(\prod b_i^{e_i} \le 2^S\) with \(S = \sum e_i \lceil \log_2 b_i \rceil\), so at most \(S + 1\) bits, S + 1 exactly where the product is \(2^S\); none for an empty factor; saturating. The same fold as count, in the other monoid: count folds \(b^e\) by \(\times\), this folds its image under CeilLog2 by \(+\), and the lax homomorphism between them is the bound. An abstract interpretation (Cousot and Cousot): the abstraction of a Galois connection between sets of values and their widths (IsGaloisConnection), sound by the adjunction. \(\mathbb{N}\) is the filtered colimit of the words \(\mathbb{N}_{<2^8} \hookrightarrow \mathbb{N}_{<2^{16}} \hookrightarrow \cdots\) (:filtered), and a finite count is compact, so it factors through a finite stage: this says which, before the count is computed (#1134).
template<HasNNOStep C, IsArrow F, IsCountWord N>
constexpr std::optional< N >	dedekind::category::exact_count (const FreeMonoid< C, F, N > &m)
constexpr auto	dedekind::category::bit_patterns (std::size_t n)
	The bit patterns of width n as a chain: the counts below \(2^n\), which binary numeration makes the words of \(\mathbb{B}^n\), bit i the letter at position i. No pattern is built: an arrow along the chain reads it. Refused past the word, where the patterns are no sequence a std::size_t can index. Counting by the laws never builds a pattern at any width; a pattern is packed only where an operation reads it, at any width known at compile time, and at run time up to max_packed_width (wider, in blocks, is #1109).
template<typename F> requires std::invocable<const F&, std::integral_constant<std::size_t, 8>>
constexpr auto	dedekind::category::with_width (std::size_t n, const F &f)
	A width known only at run time, dispatched to the narrowest precompiled bit word that holds it: 8, 16, 32 or 64 bits, a machine word, or 128, 256 or 512, a std::bitset. f is called with the width as a type, so it can name BitWord of it. Refused past max_packed_width.
template<std::unsigned_integral B> requires (!std::same_as<B, bool>)
constexpr std::size_t	dedekind::category::popcount (B x)
	The number of bits set in a machine word: the hardware's count, one instruction where the target has it.
template<std::size_t W>
constexpr std::size_t	dedekind::category::popcount (const std::bitset< W > &x)
	The number of bits set in a std::bitset.
template<HasNNOStep C, IsArrow F, IsCountWord N>
constexpr AtMost< Factor< N >, 1 >	dedekind::category::count_factors (const Power< C, F, N > &p)
	The factors of a tensor power's count: the filtered alphabet's count, its packed characteristic function's popcount, raised to the length, by the box law.
template<HasNNOStep C, IsArrow F, IsCountWord N, typename S, IsArrow T> requires HasCycleType<S, N>
constexpr auto	dedekind::category::count_factors (const Symmetric< Power< C, F, N >, S, T > &s)
	The factors of a symmetric section's count: one merged leg per cycle of sigma, so the box law after the merges, the count Pólya's theorem gives for the words a permutation fixes.
template<IsCountWord N = std::size_t>
constexpr Window< N >	dedekind::category::window (std::type_identity_t< N > offset, std::type_identity_t< N > length)
template<HasNNOStep C, IsArrow F, IsCountWord N, typename S> requires requires(const S& s) { { detail_periodic::power_of(s) } -> std::same_as<Power<C, F, N>>; } && std::equality_comparable<F>
constexpr Cylinder< Power< C, F, N >, S, N >	dedekind::category::cylinder (const Power< C, F, N > &p, Window< N > w, S s)
template<HasNNOStep C, IsArrow F, IsCountWord N, typename S> requires requires(const S& s) { requires detail_periodic::IsBoundedFactorsOf<decltype(count_factors(s)), N>; }
constexpr auto	dedekind::category::pushed_down (const Cylinder< Power< C, F, N >, S, N > &c)
	The plan of a cylinder, its selection pushed down. A cylinder in Tarski's sense, a predicate on a product in which only some legs constrain: the window's legs must lie in the set, the others are free. So the predicate moves onto the window's factor, \(\sigma_\varphi(W \times F) = \sigma_\varphi(W) \times F\), and the cylinder is the set times the power on the free legs, an outer product, whatever the window's offset. Defined where the window fits.
template<HasNNOStep C, IsArrow F, IsCountWord N, typename S> requires requires(const S& s) { requires detail_periodic::IsBoundedFactorsOf<decltype(count_factors(s)), N>; }
constexpr auto	dedekind::category::count_factors (const Cylinder< Power< C, F, N >, S, N > &c)
	The factors of a cylinder's count, aggregate pushdown (eager aggregation: Yan and Larson, VLDB 1995), derived rather than stated: the selection pushed down (pushed_down), then the box law of the outer product, the set's count times \(|\Sigma|^{N - n}\) for the free legs. Empty where no word's window can lie in the set: a window past the end, or a set of words of another length.
template<HasNNOStep C, IsArrow F, IsCountWord N, typename S> requires requires(const S& s) { { detail_periodic::power_of(s) } -> std::same_as<Power<C, F, N>>; requires detail_periodic::IsBoundedFactorsOf<decltype(count_factors(s)), N>; } && std::equality_comparable<F>
constexpr N	dedekind::category::occurrences (const Power< C, F, N > &p, const S &s)
	How often a set of words occurs in the words of a tensor power, counted with their positions: the pairs (word, offset) whose window lies in s, the sum over the offsets of the cylinders' counts, modulo the word. Each summand is pushed down (R2), so none depends on its offset: the summand has period 1, and the periodic sum takes one of them, times the number of offsets.
template<HasNNOStep C, IsArrow F, IsCountWord N, typename S> requires requires(const S& s) { { detail_periodic::power_of(s) } -> std::same_as<Power<C, F, N>>; requires detail_periodic::IsBoundedFactorsOf<decltype(count_factors(s)), N>; } && std::equality_comparable<F>
constexpr std::optional< N >	dedekind::category::exact_occurrences (const Power< C, F, N > &p, const S &s)
	The occurrences exactly, or none where the word cannot hold them: never wrapped, the discipline of exact_count.
template<typename Less, typename X, typename Y>
consteval bool	dedekind::category::lattice_definitely_less ()
	Did the comparator decide definitely True? (Unknown/False ⟹ don't reorder: keep authoring order.).
template<typename A> requires std::semiregular<std::decay_t<A>>
constexpr Maybe< std::decay_t< A > >	dedekind::category::η (maybe_monad_tag, A value)
template<typename A> requires std::semiregular<A>
constexpr Maybe< A >	dedekind::category::μ (maybe_monad_tag, Maybe< Maybe< A > > const &mma)
template<typename A> requires IsSpecies<std::decay_t<A>>
constexpr std::tuple< std::decay_t< A > >	dedekind::category::η (tuple_monad_tag, A value)
	The std::tuple<T> Frobenius monad.
template<typename A> requires IsSpecies<A>
constexpr std::tuple< A >	dedekind::category::μ (tuple_monad_tag, std::tuple< std::tuple< A > > const &tta)
template<typename A> requires IsSpecies<A>
constexpr A	dedekind::category::ε (tuple_monad_tag, std::tuple< A > const &ta)
template<typename A> requires IsSpecies<A>
constexpr std::tuple< std::tuple< A > >	dedekind::category::δ (tuple_monad_tag, std::tuple< A > const &ta)
template<typename A> requires IsSpecies<std::decay_t<A>>
constexpr Identity< std::decay_t< A > >	dedekind::category::η (identity_monad_tag, A value)
template<typename A> requires IsSpecies<A>
constexpr Identity< A >	dedekind::category::μ (identity_monad_tag, Identity< Identity< A > > const &iia)
template<typename A> requires IsSpecies<A>
constexpr Identity< A >	dedekind::category::ε (identity_monad_tag, Identity< A > const &ia)
template<typename A> requires IsSpecies<A>
constexpr Identity< Identity< A > >	dedekind::category::δ (identity_monad_tag, Identity< A > const &ia)
template<typename A, typename B>
constexpr auto	dedekind::category::constant (B y)
	The constant arrow's factory, beside id<A>() and endo<A>(f): the domain named, the codomain the value's.
template<std::equality_comparable A>
constexpr Equals< A >	dedekind::category::equals (A x)
	The equality test's factory.
template<std::same_as< Percentage > P>
constexpr P	dedekind::category::operator&& (P a, P b) noexcept
	The logical register on Percentage, as Ternary has below: && / || / ! are the species' AND / OR / RFL, so a Percentage answer conjoins as an answer (a product's membership a(x.first) && b(x.second) stays a Percentage) and HasLogicalOperators holds. Deduced on both operands, so no int → Percentage conversion sneaks a bare number into the register.
template<std::same_as< Percentage > P>
constexpr P	dedekind::category::operator|| (P a, P b) noexcept
template<std::same_as< Percentage > P>
constexpr P	dedekind::category::operator! (P a) noexcept
constexpr Ternary	dedekind::category::operator&& (Ternary a, Ternary b)
constexpr Ternary	dedekind::category::operator|| (Ternary a, Ternary b)
constexpr Ternary	dedekind::category::operator! (Ternary a)
constexpr Ternary	dedekind::category::successor (Ternary a) noexcept
	K₃'s step: the cover False → Unknown → True, saturating at the top (and its dual at the bottom), the NNO step of the chain (:nno).
constexpr Ternary	dedekind::category::predecessor (Ternary a) noexcept
constexpr std::strong_ordering	dedekind::category::operator<=> (Ternary a, Ternary b) noexcept
	Truth-order <=> on Ternary: the chain False (-1) < Unknown (0) < True (1).
template<typename TargetLogic, typename T> requires LiftableInto<T, TargetLogic>
constexpr auto	dedekind::category::lift_logic (T value)
	Lift an answer along the dominance into TargetLogic::Ω. A value already in TargetLogic::Ω passes through; otherwise its species is read off the answer type (classifier_logic_t) and the registered embedding applies. Constrained, so an unsupported lift is a substitution failure at the call site, not an error inside.
template<typename L>
constexpr bool	dedekind::category::holds (Truth< L > proposition) noexcept
	Semantic truth projection for assertion contexts.
template<typename L>
constexpr bool	dedekind::category::refutes (Truth< L > proposition) noexcept
	Semantic falsity projection for assertion contexts.
template<typename L> requires IsOckhamAlgebra<L> && logic_negation_is_involutive_v<L> && std::equality_comparable<typename L::Ω>
constexpr bool	dedekind::category::is_decided (typename L::Ω value)
	Membership in the decided core \(\{\top, \bot\}\) of an answer-lattice \(\Omega\) — the Rosolini dominance \(\Sigma\), which the paper and lift_logic define as exactly the decided subobject \(\{\top,\bot\} \hookrightarrow \Omega\).
template<std::size_t K, IsCountWord N> requires (K >= 2)
constexpr RunList< N, K >	dedekind::category::run (N lo, std::type_identity_t< N > hi)
template<typename T>
constexpr auto	dedekind::category::reduced (const T &t)
template<IsCountWord N, std::size_t J, std::size_t K>
constexpr RunList< N, J+K >	dedekind::category::operator| (const RunList< N, J > &a, const RunList< N, K > &b)
	The union of two run lists, at once: the lattice's Join node folded by the one reducer, the sweep its leaf-combine, as the set grammar's | folds through SetCombine (sets). Its bound is the sum of theirs. The strict form; the lazy one is the node itself, built and reduced later, as the predicates that opt in to :lattice's | keep it (#1138).
template<IsCountWord N, std::size_t J, std::size_t K>
constexpr RunList< N, J+K >	dedekind::category::operator& (const RunList< N, J > &a, const RunList< N, K > &b)
	The intersection, dual to the union; with a single run, by law a restriction.
template<std::size_t K, IsCountWord N, typename Pred> requires std::predicate<const Pred&, N>
constexpr Maybe< RunList< N, K > >	dedekind::category::run_list (N end, Pred holds)
	The run list of a predicate on \([0, \mathit{end})\): every count tested once, a step where the value changes.
template<IsCountWord N, std::size_t J, std::size_t K>
constexpr auto	dedekind::category::as_pullback (const RunList< N, J > &a, const RunList< N, K > &b)
	The intersection as the pullback of the two inclusions into the counts, category's apex view over it (IsPullback): in the thin category of run lists, the meet is the pullback.
template<IsCountWord N, std::size_t J, std::size_t K>
constexpr auto	dedekind::category::as_pushout (const RunList< N, J > &a, const RunList< N, K > &b)
	The union as the pushout, dual to as_pullback (IsPushout).
template<std::size_t K, IsCountWord N, std::size_t J>
constexpr Maybe< RunList< N, K > >	dedekind::category::narrowed (const RunList< N, J > &r)
	A run list under a bound claimed, not proved by the types: the same set where its steps fit, nothing where they do not.
template<IsCountWord N, std::size_t K>
constexpr RunList< N, K >	dedekind::category::preimage (const Shift< N > &t, const RunList< N, K > &s)
	preimage(shift(d), s): the pullback of s along the translation, \(x \mapsto s(x + d)\), in closed form, a run list again: the closed-form overload of :morphism's preimage(f, P), whose general form is the composite P∘f, as algebra's halfspace_transport gives one for an interval. The translation is read as a map of the chain, on its extent: the counts \(x\) with \(x + d\) below the word's top (extent in :periodic, where a shift's law holds), where the word does not wrap. halfspace_transport gates the same reading by the carrier's type (an ordered group, or ℕ, where \(x + k\) misses \(\{0, \ldots, k - 1\}\)); on the word, Pst's carrier, the extent is that gate, by value. The elements of s below d, whose preimages would wrap past the top, lie outside it and are not reported; the derivative (:automaton) meets its operand with the letter's interval first, so none exist there. The other reading, the word as the cyclic group \(\mathbb{Z}/2^w\) whose translation wraps, is order's translate (an image, a run through the end splitting in two) and morphologies' congruence preimage; it is a different arrow, and not this one (#1138).
template<IsCountWord N, std::size_t K>
constexpr RunList< N, K >	dedekind::category::operator>> (const Shift< N > &t, const RunList< N, K > &s)
	shift(d) >> s, the spelling of the preimage: precomposition with the translation.
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; }
constexpr bool	dedekind::category::symmetric_at (const Rel &rel, const T &a, const T &b)
	Symmetry at a point (mereology__The_Laws_At_A_Point).
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { successor(x) } -> std::convertible_to<T>; }
constexpr bool	dedekind::category::symmetric_on (const Rel &rel, const T &lo, const T &hi)
	Symmetry over a whole chain (mereology__The_Laws_On_A_Chain).
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { x == x } -> std::convertible_to<bool>; }
constexpr bool	dedekind::category::equality_at (const Rel &rel, const T &a, const T &b)
	Equality at a point: the relation answers as == does.
template<std::semiregular Op>
constexpr Lifted< Op >	dedekind::category::lifted (Op op)
template<IsArrow P> requires std::same_as<Cod<P>, bool>
constexpr Where< P >	dedekind::category::where (P p)
template<detail_comprehension::IsForeignView R, IsArrow F> requires std::invocable<const F&, std::ranges::range_reference_t<R>>
constexpr auto	dedekind::category::operator>> (R r, F f)
	r >> f on a range of the caller's: f on each element, which is std::views::transform.
constexpr Windows	dedekind::category::windows (std::size_t n)
template<detail_comprehension::IsForeignView R> requires std::ranges::forward_range<R>
constexpr auto	dedekind::category::operator>> (R r, Windows w)
template<typename T, IsPrefixKernel< T > K>
constexpr auto	dedekind::category::scan (K k, std::span< const T > s)
	scan(k, s), the extension of the history comonad: a kernel asked at every non-empty prefix, SQL's window function over ROWS UNBOUNDED PRECEDING, as scan on a Path (:sequences). Every position has a prefix, so unlike a window of n this is a comonad on a finite range; each answer may read the whole prefix, so a kernel that factors through finitely many states has an overload of its own (:automaton).
template<typename P, typename S, IsArrow T>
constexpr auto	dedekind::category::where (const Symmetric< P, S, T > &s)
	where(section): the windows a section holds, its membership as the filter, where(sites). The section stays a tensor (its * is the outer product); only here is it read as a predicate, its characteristic map, an arrow from a window of its letters: a std::span, since an arrow has one domain and a text is contiguous (a genome's bytes, Listing 5's carrier). The membership itself reads any random-access range; a window of a non-contiguous container is tested by it directly, not through this stage.
template<detail_comprehension::IsForeignView R, typename P, typename S, IsArrow T> requires requires(R r, const Symmetric<P, S, T>& s) { std::move(r) >> windows(1uz) >> where(s); }
constexpr auto	dedekind::category::operator>> (R r, const Symmetric< P, S, T > &s)
	r >> s: where the words of a section occur in a range of the caller's: its windows of the section's length, each kept where the section holds it. The section knows its length, so no window of another arises. Listing 5's dna >> pali6, the same expression as the join below read at one sequence.
template<std::regular S, std::semiregular Coalg, IsArrow F> requires detail_comprehension::ReadsItsElements<unfold_view<S, Coalg>, F>
constexpr auto	dedekind::category::operator>> (const unfold_view< S, Coalg > &q, F f)
	>> f on a query, SQL's SELECT: f on the present elements, the holes passed through, Maybe's action on the arrow (maybe_functor).
template<std::regular S, std::semiregular Coalg, IsArrow F> requires detail_comprehension::ReadsItsElements<unfold_view<S, Coalg>, F> && detail_comprehension::IsMaybe<Cod<F>>
constexpr auto	dedekind::category::operator>> (const unfold_view< S, Coalg > &q, F f)
	>> f on a query with f a Kleisli arrow into Maybe, a second where among them: Kleisli composition, f extended by Maybe's κ (:kleisli), so the holes do not nest. Filter fusion, where(p) >> where(q) = where(p ∧ q), is then the monad's associativity, not a rewrite of this partition's.
template<IsCountWord N, typename P, typename Q> requires requires(const P& p, const Q& q) { { p & q } -> IsArrow; requires std::same_as<Cod<decltype(p& q)>, bool>; }
constexpr auto	dedekind::category::operator>> (const FiniteChainSequence< N, Where< P > > &q, const Where< Q > &w)
	where(p) >> where(q) on a chain, fused by type: one where whose predicate is the lattice term p & q, the meet in the Boolean algebra of the chain's subobjects (:lattice's Meet). The filter is then a term the lattice's laws and the periodic counts read, not two walks; where p & q is not formed, the Kleisli composite above takes the query.
template<IsCountWord N, HasPeriod P> requires std::same_as<Cod<P>, bool>
constexpr N	dedekind::category::count (const FiniteChainSequence< N, Where< P > > &q)
	The count of a chain under a periodic filter: the count of the filter's characteristic sequence, which :periodic takes period by period (the lcm for a meet), no walk of the query. The law count(where(p)) = count(χ_p), used as the rewrite.
template<IsCountWord N = std::size_t, IsQuery Q>
constexpr N	dedekind::category::count (Q q)
	The count of a query, SQL's COUNT: its present elements, the tally lifted through Maybe.
template<IsQuery Q, IsCountWord N = typename std::ranges::range_value_t< Q>::value_type>
constexpr N	dedekind::category::sum (Q q)
	The sum of a query of counts, SQL's SUM: + lifted through Maybe.
template<HasNNOStep C, IsArrow F, IsCountWord N, typename P, typename S, IsArrow T> requires requires(const Power<C, F, N>& p, const Symmetric<P, S, T>& s) { occurrences(p, s); }
constexpr WindowJoin< Power< C, F, N >, Symmetric< P, S, T > >	dedekind::category::operator>> (const Power< C, F, N > &p, const Symmetric< P, S, T > &s)
template<IsCountWord N>
constexpr AtMost< Factor< N >, 1 >	dedekind::category::count_factors (const Offsets< N > &o)
template<typename P, typename S> requires requires(const P& p, const S& s) { occurrences(p, s); }
constexpr auto	dedekind::category::explain (const WindowJoin< P, S > &j)
	The plan of a join on the window, EXPLAIN: the offsets times the cylinder at the first, an outer product, the cylinder in turn its selection pushed down (pushed_down). Fubini, periodicity and the box law compose into it; none of the three is stated for joins. Its type is the plan, so a test asserts it. Defined where a window fits.
template<typename P, typename S> requires requires(const P& p, const S& s) { occurrences(p, s); }
constexpr auto	dedekind::category::count_factors (const WindowJoin< P, S > &j)
	The factors of a join's count: its plan's, the box law throughout, with no sum over the offsets left; none where no window fits.
template<typename P, typename S> requires requires(const P& p, const S& s) { occurrences(p, s); }
constexpr auto	dedekind::category::count (const WindowJoin< P, S > &j)
template<typename P, typename S> requires requires(const P& p, const S& s) { occurrences(p, s); }
constexpr auto	dedekind::category::exact_count (const WindowJoin< P, S > &j)
template<typename P>
constexpr detail_comprehension::JoinWithStage< P >	dedekind::category::join_with (P p)
template<IsArrow Fam, typename P> requires requires(const P& p, const Cod<Fam>& s) { occurrences(p, s); }
constexpr auto	dedekind::category::operator>> (const Fam &fam, const detail_comprehension::JoinWithStage< P > &st)
template<IsArrow F> requires requires(const Cod<F>& j) { count(j); }
constexpr auto	dedekind::category::operator>> (const F &f, detail_comprehension::CountingStage)
template<IsQuery Q>
constexpr std::size_t	dedekind::category::operator>> (Q q, detail_comprehension::CountingStage)
	q >> counting, the stage form of count(q): the fold that ends a query, in the query's own rhythm.
template<IsQuery Q>
constexpr Maybe< std::size_t >	dedekind::category::count (const Maybe< Q > &q)
	A query that may not be (a plan past its capacity), counted: the count lifted through Maybe, nothing where the query is nothing. The monad carries the uncertainty to the end, so no caller cases on it.
template<IsQuery Q>
constexpr Maybe< std::size_t >	dedekind::category::operator>> (const Maybe< Q > &q, detail_comprehension::CountingStage)
	The stage form of the same.
template<typename Order = ascending, IsArrow Rank> requires std::strict_weak_order<const Order&, Cod<Rank>, Cod<Rank>>
constexpr OrderBy< Rank, Order >	dedekind::category::order_by (Rank rank, Order order={})
template<std::size_t K>
constexpr Take< K >	dedekind::category::take ()
template<IsCountWord N, typename F, IsArrow Rank, typename Order> requires std::same_as<Dom<Rank>, N> && detail_comprehension::AscendsByPosition<F> && detail_comprehension::KeptByTheWalk<Rank, Order>
constexpr FiniteChainSequence< N, F >	dedekind::category::operator>> (const FiniteChainSequence< N, F > &q, const OrderBy< Rank, Order > &)
	order_by on a filtered chain whose rank keeps the walk's order: the identity, the query sorted by construction (rewrite 3).
template<IsCountWord N, typename F, IsArrow Rank, typename Order> requires std::same_as<Dom<Rank>, N> && detail_comprehension::AscendsByPosition<F> && detail_comprehension::ReversedByTheWalk<Rank, Order>
constexpr auto	dedekind::category::operator>> (const FiniteChainSequence< N, F > &q, const OrderBy< Rank, Order > &)
	order_by on a filtered chain whose rank reverses the walk's order: the query re-rooted on the ascending slice [0, n), read upwards, the positions where the walk read them downwards (rewrite 3).
template<std::ranges::input_range Q, IsArrow Rank, typename Order>
constexpr detail_comprehension::Pending< Q, Rank, Order >	dedekind::category::operator>> (Q q, OrderBy< Rank, Order > by)
	order_by with no law to read: pending its take.
template<std::regular S, std::semiregular Coalg, std::size_t K>
constexpr auto	dedekind::category::operator>> (const unfold_view< S, Coalg > &q, Take< K >)
	take<K> on a query or a sequence: the walk, until K elements are present, lazily (rewrite 1; on a sorted query, rewrite 3's first K).
template<typename Q, typename Rank, typename Order, std::size_t K>
constexpr auto	dedekind::category::operator>> (detail_comprehension::Pending< Q, Rank, Order > p, Take< K >)
	order_by >> take<K> with no law: fused, one pass keeping the best K in an AtMost, never sorting the whole (rewrite 2). A query still, each element present, so its count is its rows' and collect makes the plain list.
template<IsCountWord N, typename Rank, std::size_t K> requires std::same_as<Dom<Rank>, N> && antitone_on_even_lengths<Rank>::value
constexpr auto	dedekind::category::operator>> (const detail_comprehension::Pending< unfold_view< std::optional< N >, detail_chain::SliceStep< N, Where< Congruent< N > > > >, Rank, descending > &p, Take< K >)
	The lengths in a residue class, ranked by their occurrences, the first K: one plan compiled, the even case, and the run time only reindexing into it. A family whose density falls along the even lengths ranks them by construction, the shortest first (the walk read upwards, rewrite 3), so the first K need no rank evaluated at all. A residue class of even modulus holds lengths of one parity: even ones are the case; odd ones occur nowhere (the reversal pairs the letters, and no even alphabet fixes them all), all ranked alike. Either way the class's members in order are the plan, a progression: padded into the class by \(j \mapsto m j + r\), unpadded by reading the lengths back. An odd modulus mixes the parities and takes the fused pass.
template<std::regular S, std::semiregular Coalg> requires detail_comprehension::IsBounded<Coalg>
constexpr auto	dedekind::category::collect (const unfold_view< S, Coalg > &q)
	A query's present elements as a value, bounded by its take: the ext boundary, where a list is asked for (#1133). A plain sequence's elements as they are, a query's unwrapped.
template<typename Dagger, typename Op, typename T> requires std::equality_comparable<T> && requires(const T& g) { Op{}(Dagger{}(g), g); unit<T>(Op{}); }
constexpr bool	dedekind::category::is_isometry (const T &f)
	CRUCIAL (load-bearing across the library): "the converse @b is the inverse" — unitarity — is a property of an arrow (a value), not of a type. This is why the retired is_unitary certificate was wrong, and why the surface below is two coordinated forms of one computed law.
template<typename Dagger, typename Op, typename T> requires std::equality_comparable<T> && requires(const T& g) { Op{}(g, Dagger{}(g)); unit<T>(Op{}); }
constexpr bool	dedekind::category::is_coisometry (const T &f)
	The coisometry law: \(f \circ f^\dagger = \mathrm{id}\) — the dagger is a right inverse.
template<typename Dagger, typename Op, typename T>
constexpr bool	dedekind::category::is_unitary (const T &f)
	The unitary law: isometry and coisometry, hence \(f^\dagger = f^{-1}\) (a dagger-iso). Generalises the permutation's P° ; P = Δ check: the one predicate reads as "the converse is the inverse" (bijection, Mat(𝔹)), "the transpose is the inverse" (orthogonal, Mat(ℝ)) and "the adjoint is the inverse" (unitary, Mat(ℂ)) — the real / complex face of the same law.
template<typename MA, typename F> requires requires(MA const& ma, F&& f) { μ(detail_kleisli::lifted(ma, std::forward<F>(f))); }
constexpr auto	dedekind::category::κ (MA const &ma, F f)
	κ (kappa): Kleisli bind (monadic extension).
template<typename WA, typename F> requires requires(WA const& wa, F&& f) { detail_kleisli::lifted(δ(wa), std::forward<F>(f)); }
constexpr auto	dedekind::category::σ (WA const &wa, F f)
	σ (sigma): Co-Kleisli extend (comonadic extension).
template<typename MonadTag, typename MA, typename F> requires IsDefaultMonadTag<MonadTag> && requires(MonadTag tag, MA const& ma, F&& f) { μ(tag, detail_kleisli::lifted(ma, std::forward<F>(f))); }
constexpr auto	dedekind::category::κ (MonadTag tag, MA const &ma, F f)
	κ with explicit monad-tag dispatch.
template<typename MonadTag, typename WA, typename F> requires IsDefaultMonadTag<MonadTag> && requires(MonadTag tag, WA const& wa, F&& f) { detail_kleisli::lifted(δ(tag, wa), std::forward<F>(f)); }
constexpr auto	dedekind::category::σ (MonadTag tag, WA const &wa, F f)
	σ with explicit monad-tag dispatch.
template<std::ranges::input_range R, typename TA, typename Step> requires detail_kleisli::IsKleisliStep<Step, TA, std::ranges::range_value_t<R>>
constexpr TA	dedekind::category::fold (R r, TA ta, Step step)
template<typename MA, typename F> requires requires(MA const& ma, F&& f) { { κ(ma, std::forward<F>(f)) }; }
constexpr auto	dedekind::category::operator>>= (MA const &ma, F f)
	operator>>= : Monadic bind (Kleisli arrow application).
template<typename WA, typename F> requires requires(WA const& wa, F&& f) { { σ(wa, std::forward<F>(f)) }; }
constexpr auto	dedekind::category::operator<<= (WA const &wa, F f)
	operator<<= : Comonadic extend (co-Kleisli arrow application).
template<IsArrow F, IsArrow G>
constexpr auto	dedekind::category::legs (const Compose< F, G > &c)
	The legs of a composite: the arrows it composes.
template<typename β, typename T> requires Steers<β, T> || IsTermNode<T> || std::invocable<const β&, const T&>
constexpr auto	dedekind::category::cata (const β &alg, const T &t)
	cata ⦇β⦈ — the catamorphism (fold): the unique F-algebra homomorphism from the initial algebra (the term itself, μF) into an algebra (B, β).
template<typename β, typename T, std::size_t... I> requires IsTermNode<T> && std::invocable< const β&, const T&, decltype(cata(std::declval<const β&>(), std::get<I>(legs(std::declval<const T&>()))))...>
constexpr auto	dedekind::category::detail_f_algebra::fold_legs (const β &alg, const T &t, std::index_sequence< I... >)
template<typename A>
constexpr A	operator() (const A &atom) const
template<typename N, typename... R> requires requires(const N& n, const R&... r) { reduce_β(n, r...); }
constexpr auto	operator() (const N &node, const R &... reduced) const
template<typename A>
constexpr ArrowLaws	operator() (const A &) const
template<typename N, typename R0, typename... R>
constexpr ArrowLaws	operator() (const N &, const R0 &, const R &...) const
template<typename F, typename G>
constexpr ArrowLaws	operator() (const Compose< F, G > &, const ArrowLaws &f, const ArrowLaws &g) const
template<typename A, typename F, typename B, typename G> requires (IsPairProjection<A, 1> && IsPairProjection<B, 2>)
constexpr ArrowLaws	steer (const Pairing< Compose< A, F >, Compose< B, G > > &t) const
	The defining forms of × and +, recognised before the fold descends (cata's steer): the product (sum) fact on the factors, which the pairing (copairing) rule alone would lose.
template<typename F, typename G, typename X, typename Y>
constexpr ArrowLaws	steer (const Copairing< Compose< F, Injection< 1, X, Y > >, Compose< G, Injection< 2, X, Y > > > &t) const
template<typename F, typename G>
constexpr ArrowLaws	operator() (const Pairing< F, G > &, const ArrowLaws &f, const ArrowLaws &g) const
template<typename F, typename G>
constexpr ArrowLaws	operator() (const Copairing< F, G > &, const ArrowLaws &f, const ArrowLaws &g) const
template<IsArrow T>
constexpr auto	dedekind::category::cata (const T &t)
	cata(t): the term rewritten to its normal form under the β-reduction algebra. simplify is cata. The IsArrow gate keeps a bare product out of the term universe.
template<typename T, typename Policy> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr Ternary	dedekind::category::classify_numeric (T x, Policy policy)
	Classify a numeric value under a user policy.
template<std::integral T, typename Policy> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr NumericWitness< T >	dedekind::category::certify_add (T a, T b, Policy policy)
	Certified integer addition with an explicit support policy.
template<std::floating_point T, typename Policy = NaNHolePolicy<T>> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr NumericWitness< T >	dedekind::category::certify_add (T a, T b, Policy policy={})
	Certified floating addition with NaN-hole policy.
template<std::integral T, typename Policy> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr NumericWitness< T >	dedekind::category::certify_mul (T a, T b, Policy policy)
	Certified integer multiplication with an explicit support policy.
template<std::floating_point T, typename Policy = NaNHolePolicy<T>> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr NumericWitness< T >	dedekind::category::certify_mul (T a, T b, Policy policy={})
	Certified floating multiplication with NaN-hole policy.
template<std::integral T, typename Policy> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr NumericWitness< T >	dedekind::category::certify_div (T a, T b, Policy policy)
	Certified integer division with explicit policy.
template<std::floating_point T, typename Policy = NaNHolePolicy<T>> requires IsLipschitzBoundaryPolicy<Policy, T>
constexpr NumericWitness< T >	dedekind::category::certify_div (T a, T b, Policy policy={})
	Certified floating division with NaN-hole policy.
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< int >	dedekind::category::certify_add_int_interval (int a, int b, IntervalBoundaryPolicy< int > policy)
	Non-template bridge functions for profiler-friendly attribution.
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< unsigned int >	dedekind::category::certify_add_uint_full (unsigned int a, unsigned int b, FullMachineBoundaryPolicy< unsigned int > policy={})
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< int >	dedekind::category::certify_mul_int_interval (int a, int b, IntervalBoundaryPolicy< int > policy)
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< int >	dedekind::category::certify_div_int_full (int a, int b, FullMachineBoundaryPolicy< int > policy={})
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< double >	dedekind::category::certify_add_double_nan (double a, double b, NaNHolePolicy< double > policy={})
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< double >	dedekind::category::certify_mul_double_nan (double a, double b, NaNHolePolicy< double > policy={})
DEDEKIND_BRIDGE_NOINLINE DEDEKIND_BRIDGE_CONSTEXPR NumericWitness< double >	dedekind::category::certify_div_double_nan (double a, double b, NaNHolePolicy< double > policy={})
template<typename A, typename B> requires detail_lattice_nodes::BuildNodes<A, B>
constexpr Join< A, B >	dedekind::category::operator| (A a, B b)
template<typename A, typename B> requires detail_lattice_nodes::BuildNodes<A, B>
constexpr Meet< A, B >	dedekind::category::operator& (A a, B b)
template<typename A, typename B>
constexpr A	dedekind::category::component (const Meet< A, B > &m, At< 1 >)
	π_1: the left-operand accessor of a binary node, returned by const-reference. The operand may itself be a whole set expression (a nested node), and π_1 / π_2 are pure projections. They must not copy the sub-structure. When the operand is a set, π_1(node) is then a bona fide reference to that IsSet (the downstream sets lift relies on this). Still ->convertible_to , so IsProduct is satisfied.
template<typename A, typename B>
constexpr B	dedekind::category::component (const Meet< A, B > &m, At< 2 >)
	π_2: the right-operand accessor of a meet, by const-reference (see π_1).
template<typename A, typename B>
constexpr A	dedekind::category::component (const Join< A, B > &j, At< 1 >)
	π_1: the left-operand accessor of a join, by const-reference (see the meet overload).
template<typename A, typename B>
constexpr B	dedekind::category::component (const Join< A, B > &j, At< 2 >)
	π_2: the right-operand accessor of a join, by const-reference.
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::meet_bounded_law (const RA &a, const RB &b)
	Law induced by a bounded lattice (IsBoundedLatticeCategory): the unit and annihilator. Meet: ⊥∧X=⊥ (annihilator), ⊤∧X=X (unit). Fires only when both operands share a carrier (mixed-carrier ⟹ inactive).
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::join_bounded_law (const RA &a, const RB &b)
	The join dual: ⊤∨X=⊤ (annihilator), ⊥∨X=X (unit). Likewise fires only when both operands share a carrier.
template<typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::idempotent_law (const RA &a, const RB &)
	Law induced by a (meet/join-)semilattice: idempotence X∧X=X / X∨X=X. Structural: it holds for the lattice operation itself, so it does not depend on the carrier's order. It fires even for order-incomparable opaque leaves. It is gated on idempotent_leaf_v, so a runtime-stateful leaf (two same-type-but-distinct instances) is not collapsed.
template<typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::meet_structural_absorption_law (const RA &a, const RB &b)
	Law induced by a lattice (IsLatticeCategory): structural absorption a∧(a∨b)=a. Structural like idempotence (a lattice axiom needing no order or carrier), so it fires even for order-incomparable opaque leaves; unlike the glb collapse (which needs comparable operands). One level only: nested / associatively-buried occurrences (a∧((a∨b)∨c)) await an associativity-flattening law (tracked on the reducer epic #890). Fails closed on a mixed-carrier term (has_mixed_carrier_v) so it upholds the same recursive fail-closed invariant as carrier_of / the boundary laws; the all-opaque (unknown-carrier) case still fires.
template<typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::join_structural_absorption_law (const RA &a, const RB &b)
	The join dual: a∨(a∧b)=a. Likewise fails closed on mixed carriers.
template<typename A, typename B, typename Ord>
consteval bool	dedekind::category::order_leq ()
	Is A ≤ B in the injected order Ord? (false when the pair is not compile-time comparable there — the glb/lub law then does not fire.).
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::meet_glb_law (const RA &a, const RB &b)
	Law induced by a lattice's order-meet consistency (RA≤RB ⟺ RA∧RB=RA): for ≤-comparable operands the meet is their glb (the smaller). Note this is not the structural absorption identity a∧(a∨b)=a (which needs no comparison); that is the separate meet_structural_absorption_law. Here only comparable operands collapse.
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::join_lub_law (const RA &a, const RB &b)
	The join dual: for comparable operands the join is their lub (the larger), RA≤RB ⟹ RA∨RB=RB. (Structural absorption a∨(a∧b)=a is the separate join_structural_absorption_law.).
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::meet_distributivity_law (const RA &a, const RB &b)
	Law induced by a distributive lattice: distribute meet over join, X∧(P∨Q) → (X∧P)∨(X∧Q), driving toward a join-of-meets (DNF). One direction only (meet over join, never join over meet), so re-reduction of the result — which the assembler performs — terminates. Gated on both operands sharing a carrier (SameCarrier) whose lattice is distributive under Ord; a chain is gated but pre-empted by the glb collapse, so this fires only on a genuine non-chain distributive lattice.
template<typename Ord, typename RA> requires std::copy_constructible<RA>
constexpr auto	dedekind::category::de_morgan_law (const RA &a)
	Law induced by an involutive De Morgan negation: rewrite ¬(reduced) by involution (¬¬A→A) and De Morgan (¬(A∧B)→¬A∨¬B, ¬(A∨B)→¬A∧¬B), pushing the negation toward the leaves (negation-normal form). Gated on the carrier's lattice carrying such a negation under Ord; a bare ¬leaf is already normal and stays (law_inactive). The driver re-reduces the pushed-down result (termination: ¬ strictly descends).
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::meet_complement_law (const RA &, const RB &)
	Law induced by a complemented lattice: the complement collapse a∧¬a→⊥ (meet) / a∨¬a→⊤ (join). The bottom / top produced is the carrier's registered LatticeBottom / LatticeTop over its resolved order (for sets, that is Ø / 𝔸 once the sets layer registers them). Gated on the carrier being complemented under Ord; else inactive.
template<typename Ord, typename RA, typename RB> requires std::copy_constructible<RA> && std::copy_constructible<RB>
constexpr auto	dedekind::category::join_complement_law (const RA &, const RB &)
	The join dual: a∨¬a→⊤ (excluded middle).
constexpr Columns	dedekind::category::columns_of (const Letters &on)
template<std::size_t Sigma, std::size_t P, std::size_t K, std::size_t Q, IsCountWord N, std::size_t KL>
constexpr Maybe< Automaton< Sigma, Q > >	dedekind::category::automaton (const RunList< N, KL > &sites, std::type_identity_t< N > length)
	The matcher specialised to a set of words of one length: the minimal automaton of \(\Sigma^* L\), canonical.
template<std::size_t KL, std::size_t Sigma, std::size_t P, HasNNOStep C, IsArrow F, IsCountWord N, typename S, IsArrow T>
constexpr Maybe< RunList< N, KL > >	dedekind::category::run_list (const Symmetric< Power< C, F, N >, S, T > &sites)
	A section's words as a run list over their codes: each word read as its letters' ranks in base \(\sigma\), the first the most significant, so the chain \([0, \sigma^n)\) in the dictionary order. Every code is read back as its word and tested by the section's own membership: \(\sigma^n\) tests, the set enumerated once.
template<std::size_t KL, std::size_t Sigma, std::size_t P, IsCountWord N> requires (Sigma >= 4 && Sigma % 2 == 0)
constexpr Maybe< RunList< N, KL > >	dedekind::category::run_list (const Symmetric< Power< std::byte, Letters, N >, Reverse, Reflection > &sites)
	The words a reflection then the reversal fixes, listed by the law: a word is fixed by its half-site, so the \(\sigma^{n/2}\) halves are visited in order and no word is tested, where the general overload tests all \(\sigma^n\). This is what lets a small panel's table be built at compile time. With an even alphabet the reflection fixes no letter, and from four letters no two codes are adjacent, so each is a run of its own. An odd length, or a reflection other than the alphabet's own, is left to the general overload.
template<std::size_t Sigma = 4, std::size_t P = 8, std::size_t K = 32, std::size_t Q = 320, std::size_t KL = 256, HasNNOStep C, IsArrow F, IsCountWord N, typename S, IsArrow T>
constexpr Maybe< Automaton< Sigma, Q > >	dedekind::category::automaton (const Symmetric< Power< C, F, N >, S, T > &sites)
	The matcher specialised to a section: its words as a run list, then the plan. The capacities default to a menu's largest, four letters, words of length 8, pending sets of 32 steps and 320 states, the one pynzli offers too, so automaton(sites) reads alike in both languages; a tighter bound is named where the plan is a constant.
constexpr Prefix	dedekind::category::prefix (std::string_view word)
template<typename P, typename S, IsArrow T>
constexpr Prefixed< P, S, T >	dedekind::category::operator& (const Symmetric< P, S, T > &s, const Prefix &p)
template<std::size_t KL, std::size_t Sigma, std::size_t P, IsCountWord N> requires (Sigma >= 4 && Sigma % 2 == 0)
constexpr Maybe< RunList< N, KL > >	dedekind::category::run_list (const Prefixed< Power< std::byte, Letters, N >, Reverse, Reflection > &sites)
	The words of a section beginning with a prefix, by the law: no word tested, only the half-sites the prefix allows visited.
template<std::size_t Sigma = 4, std::size_t P = 8, std::size_t K = 32, std::size_t Q = 320, std::size_t KL = 256, IsCountWord N>
constexpr Maybe< Automaton< Sigma, Q > >	dedekind::category::automaton (const Prefixed< Power< std::byte, Letters, N >, Reverse, Reflection > &sites)
	The matcher of the words of a section beginning with a prefix. The same builder on a subset of the same words; capacities as for a section.
template<std::size_t Sigma, std::size_t Q>
constexpr std::size_t	dedekind::category::states (const Automaton< Sigma, Q > &plan)
template<std::size_t Sigma, std::size_t Q>
constexpr Matches< Sigma, Q >	dedekind::category::matches (const Automaton< Sigma, Q > &plan, Holes holes=Holes::break_match)
template<std::size_t Sigma, std::size_t Q>
constexpr Maybe< Matches< Sigma, Q > >	dedekind::category::matches (const Maybe< Automaton< Sigma, Q > > &plan, Holes holes=Holes::break_match)
	matches on a plan that may not be, automaton(section)'s Maybe: the stage, or nothing, by Maybe's action. The uncertainty of the capacity travels through the query to its count, so dna >> matches(automaton(s)) >> counting is a Maybe count with no case on it in between.
template<std::ranges::view V, std::size_t Sigma, std::size_t Q> requires std::ranges::random_access_range<V> && std::ranges::sized_range<V> && std::semiregular<V>
constexpr auto	dedekind::category::operator>> (V letters, const Maybe< Matches< Sigma, Q > > &m)
template<std::ranges::view V, std::size_t Sigma, std::size_t Q> requires std::ranges::random_access_range<V> && std::ranges::sized_range<V> && std::semiregular<V>
constexpr auto	dedekind::category::operator>> (V letters, const Matches< Sigma, Q > &m)
template<std::ranges::view V, std::size_t Sigma, std::size_t Q> requires std::ranges::random_access_range<V> && std::ranges::sized_range<V> && std::semiregular<V>
constexpr auto	dedekind::category::scan (const Automaton< Sigma, Q > &plan, V letters)
	scan(plan, s): the history comonad's extension with its kernel factored through finitely many states, so that it keeps one state, not the history (Myhill and Nerode). It is matches(plan), its holes breaking a match.
template<std::ranges::view V, std::size_t Sigma, std::size_t Q> requires std::ranges::random_access_range<V> && std::ranges::sized_range<V> && std::semiregular<V>
constexpr auto	dedekind::category::operator>> (V letters, const Automaton< Sigma, Q > &plan)
	s >> scanner: a plan read as the stage it is.
template<detail_comprehension::IsForeignView R, typename P, typename S, IsArrow T>
constexpr auto	dedekind::category::operator>> (R r, const Prefixed< P, S, T > &s)
	Where a prefixed section's words occur in a range of the caller's: the windows of its length it holds, as r >> s for a section.
template<IsByteText R, IsCountWord N>
constexpr ReflectedWindows< R, N >	dedekind::category::operator>> (R r, const Symmetric< Power< std::byte, Letters, N >, Reverse, Reflection > &s)
	r >> s, where the law is in the section's type.
template<IsCountWord W = std::size_t, IsByteText R, IsCountWord N>
constexpr W	dedekind::category::count (const ReflectedWindows< R, N > &q)
	The count of a section fixed by reversal and reflection, without asking each window: the law says a window is independent pairs, so no position depends on another. The overload is narrow, and in practice it is DNA's and RNA's: exactly four letters, their own reflection, a word of even length up to 16. It names a law of biochemistry and no instruction of any machine. The alphabet and the length are values, here as in a binding. Any other section takes the plain fold, whose answer this one must equal.
template<typename F> requires IsIsomorphism<std::remove_cvref_t<F>> && requires(const std::remove_cvref_t<F>& cf, const Cod<F>& y) { inverse(cf)(y); }
constexpr auto	dedekind::category::retract (F f)
	Blanket retract for any IsIsomorphism: wraps inverse(f) in always-Some (see IsoRetract). This is what makes IsIsomorphism ⟹ IsRetractableArrow hold with no manual hook.
template<typename F> requires (!IsArrow<std::remove_cvref_t<F>>) && requires(F f) { typename signature_extractor<F>::type; }
constexpr auto	dedekind::category::arrow (F f)
template<typename A, typename B, typename F>
constexpr auto	dedekind::category::arrow (F f)
template<typename A, typename F> requires (!IsArrow<F> && std::invocable<std::decay_t<F>, const A&>)
constexpr auto	dedekind::category::arrow (F f)
template<typename A, typename F>
constexpr auto	dedekind::category::endo (F f)
template<typename A, typename B>
constexpr auto	dedekind::category::operator&& (const Rule< A, B > &p1, const Rule< A, B > &p2)
template<typename A, typename B>
constexpr auto	dedekind::category::operator|| (const Rule< A, B > &p1, const Rule< A, B > &p2)
template<typename A>
constexpr auto	dedekind::category::id ()
	The Identity Factory: Returns the neutral arrow for Species A.
template<IsArrow F, IsArrow P> requires std::same_as<Cod<F>, Dom<P>>
constexpr auto	dedekind::category::preimage (const F &f, const P &p)
	The contravariant substitution / pullback f*: pull a codomain predicate (or arrow) P back along f, preimage(f,P) = P∘f = Compose<F,P>.
template<IsArrow F, IsArrow G>
constexpr F	dedekind::category::component (const Compose< F, G > &c, std::integral_constant< std::size_t, 1 >)
	Product projections for the reified composite Compose<F,G>: its two legs .f / .g are the product components, so Compose<F,G> is the categorical product of its operand arrows F, G in the arrow category — which is exactly why composition PRESERVES the leg types where the old type-erasing lambda hid them. These are custom-storage overloads of the projections' component hook (:limit; the slot is :limit's At<k>, spelled out here upstream of it): storage is named .f / .g rather than .first / .second, so per the Dual val/der precedent Compose supplies its own overloads in its home namespace, found by ADL. With them IsProduct<Compose<F,G>,F,G> holds (witnessed in :limit).
template<IsArrow F, IsArrow G>
constexpr G	dedekind::category::component (const Compose< F, G > &c, std::integral_constant< std::size_t, 2 >)
template<typename F, typename G> requires IsArrow<std::decay_t<F>> && IsArrow<std::decay_t<G>> && std::same_as<typename std::decay_t<F>::Codomain, typename std::decay_t<G>::Domain>
constexpr auto	dedekind::category::operator>> (F f, G g)
	Synthesizes an arrow A -> C from A -> B and B -> C.
template<typename F, typename G> requires IsArrow<std::decay_t<F>> && IsArrow<std::decay_t<G>> && std::same_as<typename std::decay_t<F>::Codomain, typename std::decay_t<G>::Domain> && IsIdentityArrow<F>
constexpr auto	dedekind::category::operator>> (F, G g)
template<typename F, typename G> requires IsArrow<std::decay_t<F>> && IsArrow<std::decay_t<G>> && std::same_as<typename std::decay_t<F>::Codomain, typename std::decay_t<G>::Domain> && IsIdentityArrow<G>
constexpr auto	dedekind::category::operator>> (F f, G)
template<typename F, typename G> requires IsArrow<std::decay_t<F>> && IsArrow<std::decay_t<G>> && std::same_as<typename std::decay_t<F>::Codomain, typename std::decay_t<G>::Domain> && IsIdentityArrow<F> && IsIdentityArrow<G>
constexpr auto	dedekind::category::operator>> (F f, G)
template<auto f, typename T> requires IsArrow<decltype(f)>
constexpr T	dedekind::category::call (T x)
	A stateless arrow as a function: &call<F{}, T> is a pointer through which F{} is called, so that an empty arrow has a representation with one storage class (:cartesian's Morphisms).
template<typename F, typename G> requires IsArrow<std::decay_t<F>> && (!IsArrow<std::decay_t<G>>) && std::invocable<std::decay_t<G>&, const typename std::decay_t<F>::Codomain&>
constexpr auto	dedekind::category::operator>> (F f, G g)
	operator>> with a callable on the RHS — auto-wraps the lambda as arrow<F::Codomain> .
template<typename F, typename G> requires (!IsArrow<std::decay_t<F>>) && IsArrow<std::decay_t<G>> && std::invocable<std::decay_t<F>&, const typename std::decay_t<G>::Domain&> && (!std::convertible_to<F, typename std::decay_t<G>::Domain>)
constexpr auto	dedekind::category::operator>> (F f, G g)
	The same with the callable on the LHS: rev >> power(τ) gives rev the arrow's domain, as power(τ) >> rev gives it the codomain. A value on the LHS is application (below); the two do not meet, since a value convertible to the domain is not a callable on it.
template<typename F> requires is_self_inverse_v<std::remove_cvref_t<F>>
constexpr std::remove_cvref_t< F >	dedekind::category::inverse (const F &f)
	A self-inverse arrow is its own inverse.
template<typename T>
constexpr auto	dedekind::category::inverse (Identity< T > id) noexcept
	The structural inverse of an Identity is itself.
template<typename A, typename B, typename Impl> requires std::same_as<Impl, std::negate<A>>
constexpr auto	dedekind::category::inverse (Morphism< A, B, Impl > f) noexcept
	The structural inverse of Negation is itself (Involutive).
template<IsArrow F, IsArrow G> requires (IsIsomorphism<F> && IsIsomorphism<G>)
constexpr auto	dedekind::category::inverse (const Compose< F, G > &c)
	A composite of isomorphisms is one: \((g \circ f)^{-1} = f^{-1} \circ g^{-1}\), the inverses run the other way round. The rule, not a declaration per composite; with the involution rule (:involution, an involution is its own inverse) the composite of two involutions is an isomorphism, though in general no involution.
template<typename T, typename Arrow> requires IsArrow<Arrow> && std::convertible_to<T, typename Arrow::Domain>
constexpr auto	dedekind::category::operator>> (T value, const Arrow &f) -> typename Arrow::Codomain
	Proposition: A Value x can be piped into a Morphism f: A -> B.
template<typename X, typename F, typename Equal = std::equal_to<>> requires std::copyable<X> && std::regular_invocable<const F&, const X&> && std::convertible_to<std::invoke_result_t<const F&, const X&>, X> && (std::predicate<const Equal&, const X&, const X&> || std::same_as<Equal, std::equal_to<>>)
constexpr X	dedekind::category::iterate (const F &f, const X &x0, std::size_t n, const Equal &equal={})
template<typename A, typename F> requires (!IsArrow<std::remove_cvref_t<F>>) && std::invocable<std::decay_t<F>, const A&> && IsΩ<std::invoke_result_t<std::decay_t<F>, const A&>>
constexpr auto	dedekind::category::classify (F f)
	Characteristic Morphism Factory (classify) Returns the Subobject Species (The Body) carrying the rule (The Arrow).
template<typename F> requires (!IsArrow<std::remove_cvref_t<F>>) && requires { typename signature_extractor<std::decay_t<F>>::type; } && IsΩ<codomain_t<std::decay_t<F>>>
constexpr auto	dedekind::category::classify (F f)
	Domain-inferring classify: deduces A from the callable's signature.
template<typename A, IsArrow F> requires IsPredicate<F> && std::same_as<Dom<F>, A>
constexpr auto	dedekind::category::classify (F f)
	Idempotent classify: Passthrough for existing Arrows.
template<typename P, typename Q> requires IsPredicatePair<P, Q>
constexpr auto	dedekind::category::operator&& (P p, Q q)
	Logical Conjunction (Intersection): Synthesizes a rule for A ∩ B.
template<IsClassifierConstant C, IsPredicate P> requires (!IsPredicate<std::remove_cvref_t<C>>) && requires(C c) { lift_classifier_constant<Cod<P>, predicate_logic_t<P>>(c); }
constexpr auto	dedekind::category::operator&& (C constant, P p)
	Conjunction of a constant logical value with a predicate.
template<IsPredicate P, IsClassifierConstant C> requires (!IsPredicate<std::remove_cvref_t<C>>) && requires(C c) { lift_classifier_constant<Cod<P>, predicate_logic_t<P>>(c); }
constexpr auto	dedekind::category::operator&& (P p, C constant)
	Conjunction of a predicate with a constant logical value.
template<typename P, typename Q> requires IsPredicatePair<P, Q>
constexpr auto	dedekind::category::operator|| (P p, Q q)
	Logical Disjunction (Union): Synthesizes a rule for A ∪ B.
template<IsClassifierConstant C, IsPredicate P> requires (!IsPredicate<std::remove_cvref_t<C>>) && requires(C c) { lift_classifier_constant<Cod<P>, predicate_logic_t<P>>(c); }
constexpr auto	dedekind::category::operator|| (C constant, P p)
	Disjunction of a constant logical value with a predicate.
template<IsPredicate P, IsClassifierConstant C> requires (!IsPredicate<std::remove_cvref_t<C>>) && requires(C c) { lift_classifier_constant<Cod<P>, predicate_logic_t<P>>(c); }
constexpr auto	dedekind::category::operator|| (P p, C constant)
	Disjunction of a predicate with a constant logical value.
template<IsPredicate P>
constexpr auto	dedekind::category::operator! (P p)
	Logical Negation (Complement): Synthesizes a rule for ¬A.
template<typename A, typename P, typename Q> requires std::invocable<const std::decay_t<P>&, const A&> && std::invocable<const std::decay_t<Q>&, const A&> && IsΩ<std::remove_cvref_t< std::invoke_result_t<const std::decay_t<P>&, const A&>>> && std::same_as< std::remove_cvref_t< std::invoke_result_t<const std::decay_t<P>&, const A&>>, std::remove_cvref_t< std::invoke_result_t<const std::decay_t<Q>&, const A&>>>
constexpr auto	dedekind::category::predicate_and (P p, Q q)
	Compose two plain callable predicates over a declared domain A.
template<typename A, typename P, typename Q> requires std::invocable<const std::decay_t<P>&, const A&> && std::invocable<const std::decay_t<Q>&, const A&> && IsΩ<std::remove_cvref_t< std::invoke_result_t<const std::decay_t<P>&, const A&>>> && std::same_as< std::remove_cvref_t< std::invoke_result_t<const std::decay_t<P>&, const A&>>, std::remove_cvref_t< std::invoke_result_t<const std::decay_t<Q>&, const A&>>>
constexpr auto	dedekind::category::predicate_or (P p, Q q)
	Disjunction bridge for plain callable predicates over domain A.
template<typename A, typename P> requires std::invocable<const std::decay_t<P>&, const A&> && IsΩ<std::remove_cvref_t< std::invoke_result_t<const std::decay_t<P>&, const A&>>>
constexpr auto	dedekind::category::predicate_not (P p)
	Negation bridge for plain callable predicates over domain A.
template<typename A, typename L = Boole> requires IsOckhamAlgebra<L>
constexpr auto	dedekind::category::constant_classifier (typename L::Ω value)
	Constant classifier factory over domain A: A -> Ω.
template<typename A, typename L = Boole> requires IsOckhamAlgebra<L>
constexpr auto	dedekind::category::classifier_true ()
	The tautology / top predicate \(\top\) over domain A: the canonical always-true classifier A → Ω, constant at L::True. This is the topos truth arrow \(\top: 1 \to \Omega\) pulled back to a predicate on A (verum, "everything is a member"); use it wherever a whole-domain / unrestricted characteristic map is wanted rather than an ad-hoc [](const A&){ return true; } lambda.
template<typename A, typename L = Boole> requires IsOckhamAlgebra<L>
constexpr auto	dedekind::category::classifier_false ()
	The contradiction / bottom predicate \(\bot\) over domain A: the canonical always-false classifier A → Ω, constant at L::False (falsum, "nothing is a member"). Dual of classifier_true.
template<typename A, typename L = Kleene> requires IsOckhamAlgebra<L> && requires { L::Unknown; }
constexpr auto	dedekind::category::classifier_unknown ()
	Default unknown classifier over domain A (only for logics with Unknown).
template<typename L = Boole> requires IsOckhamAlgebra<L>
constexpr auto	dedekind::category::logical_true ()
	The 'true' morphism: 1 → Ω.
template<typename L = Boole> requires IsOckhamAlgebra<L>
constexpr auto	dedekind::category::logical_false ()
	The 'false' morphism: 1 → Ω.
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; }
constexpr bool	dedekind::category::reflexive_at (const Rel &rel, const T &a)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; }
constexpr bool	dedekind::category::transitive_at (const Rel &rel, const T &a, const T &b, const T &c)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { x == x } -> std::convertible_to<bool>; }
constexpr bool	dedekind::category::antisymmetric_at (const Rel &rel, const T &a, const T &b)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; }
constexpr bool	dedekind::category::connex_at (const Rel &rel, const T &a, const T &b)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { successor(x) } -> std::convertible_to<T>; }
constexpr bool	dedekind::category::reflexive_on (const Rel &rel, const T &lo, const T &hi)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { successor(x) } -> std::convertible_to<T>; }
constexpr bool	dedekind::category::antisymmetric_on (const Rel &rel, const T &lo, const T &hi)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { successor(x) } -> std::convertible_to<T>; }
constexpr bool	dedekind::category::connex_on (const Rel &rel, const T &lo, const T &hi)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { successor(x) } -> std::convertible_to<T>; }
constexpr bool	dedekind::category::transitive_on (const Rel &rel, const T &lo, const T &hi)
template<typename Whole> requires requires { whole.operator->(); }
constexpr auto	dedekind::category::arrow_drill_down (const Whole &whole)
	Generic opt-in drill-down projector for part-whole wrappers.
template<typename T>
constexpr T	dedekind::category::arrow_drill_down (const T *whole)
	Pointer overload for generic drill-down projection.
template<typename T, typename Op> requires requires { unit_trait<T, Op>::value; }
constexpr T	dedekind::category::unit (Op)
	The unit of Op at the carrier T, read as unit<T>(Op{}).
template<typename T, typename Op> requires requires(T a) { { inverse(a, Op{}) } -> std::same_as<T>; }
constexpr T	dedekind::category::inverse_v (T a)
	The Master Bridge: Routes the request to specific implementations.
template<typename T, typename Op>
constexpr bool	dedekind::category::associative (Op)
	The laws as functions of the operation: associative<T>(Op{}), commutative<T>(Op{}), idempotent<T>(Op{}) and distributive<T>(Mul{}, Add{}).
template<typename T, typename Op>
constexpr bool	dedekind::category::commutative (Op)
template<typename T, typename Op>
constexpr bool	dedekind::category::idempotent (Op)
template<typename T, typename Mul, typename Add>
constexpr bool	dedekind::category::distributive (Mul, Add)
template<typename T, typename Rel = std::less_equal<T>, typename L = Boole, typename Project = std::identity> requires IsPathProjection<Project, T, Rel, typename L::Ω>
constexpr L::Ω	dedekind::category::check_path (T a, T b, T c, Project project={})
	Verify that a two-step path A→B→C exists in the posetal category.
template<typename Whole> requires requires { arrow_drill_down(whole).min; }
constexpr auto	dedekind::category::arrow_drill_down_min (const Whole &whole)
	Opt-in drill-down projector for min/max result carriers.
constexpr Ternary	dedekind::category::monotone (ArrowLaws p)
	What a profile says about monotonicity: the law read off the fold's result, in K₃ (True where certified, Unknown where not).
constexpr Ternary	dedekind::category::infer (ArrowLaw w, ArrowNode n, const ArrowLaws &a, const ArrowLaws &b)
	The engine at one law: a former's answer from its legs' profiles, their laws combined by the chain's own Inf (both legs) and Sup (either leg). The facts, each a theorem about functions:
constexpr ArrowLaws	dedekind::category::saturated (ArrowLaws p)
	Entailment, a closure operator on profiles: an involution is its own inverse, so a bijection. Nothing is entailed about a constant arrow's variance here: it is monotone and antitone under a reflexive order and neither under a strict one, and a profile is read under an arbitrary order; the typed reader has the fact where the order is in reach (:total). Nor the converse, monotone and antitone entailing constant, which holds on a connected domain only. The engine applies the entailment to values; a typed arrow already has it through the iso hook (:involution).
constexpr ArrowLaws	dedekind::category::without_variance (ArrowLaws p)
	The laws that do not depend on an order: a profile read under an order the former's variance facts are not about.
constexpr ArrowLaws	dedekind::category::arrow_node (ArrowNode n, const ArrowLaws &a, const ArrowLaws &b)
	The engine at a former, law by law, its legs and its answer saturated.
template<IsArrow F>
constexpr bool	dedekind::category::is_identity (const F &)
	The laws of an arrow asked on its value (the Jlt paper's Listing 1): each reads, at compile time, the registration its concept reads, so is_monic(f) is IsMonicArrow<F> at the value's type, and a composite's law comes through the readers above. A concept gates a template, a predicate states a fact; both read one registration.
template<IsArrow F>
constexpr bool	dedekind::category::is_constant (const F &)
template<IsArrow F>
constexpr bool	dedekind::category::is_monic (const F &)
template<IsArrow F>
constexpr bool	dedekind::category::is_epic (const F &)
template<IsArrow F>
constexpr bool	dedekind::category::is_iso (const F &)
template<IsArrow F>
constexpr bool	dedekind::category::is_involution (const F &)
template<IsArrow F, IsArrow G> requires commutes_v<F, G>
constexpr bool	dedekind::category::is_involution (const Compose< F, G > &c)
	A composite of two commuting involutions is one, \((g f)^2 = g g f f = \mathrm{id}\), its law derived from its legs' (commutes, :involution); where the legs do not commute, the reading above decides, and - after ~ is none.
template<IsArrow F, typename Op = std::less_equal<>>
constexpr bool	dedekind::category::is_monotone (const F &, Op={})
template<IsArrow F, typename Op = std::less_equal<>>
constexpr bool	dedekind::category::is_antitone (const F &, Op={})
template<IsArrow F> requires std::unsigned_integral<Cod<F>> && (!std::same_as<Cod<F>, bool>)
constexpr auto	dedekind::category::operator~ (const F &f)
	The involutions of a codomain, pointwise on the arrows into it: ~f and -f are f then the reflection of the chain, respectively unary minus, (-f)(x) = -f(x) as for functions in analysis; on an identity the composite is the involution itself (the unit law, :morphism). !f, for the arrows into a truth object, is in :topoi. Unsigned only: -INT_MIN is not a function on int (:involution); and not bool, which C++ counts as unsigned, so a set's characteristic arrow keeps the complement of :sets.
template<IsArrow F> requires std::unsigned_integral<Cod<F>> && (!std::same_as<Cod<F>, bool>)
constexpr auto	dedekind::category::operator- (const F &f)
template<typename F> requires IsArrow<F> && std::constructible_from<std::remove_cvref_t<F>, F&&>
constexpr auto	dedekind::category::image_of (F f)
	Factory: image_of(f) constructs the image of f as a Subobject of Cod<F>.
template<typename Left, typename Right, typename Unit, typename Counit> requires IsAdjunction<std::remove_cvref_t<Left>, std::remove_cvref_t<Right>, std::remove_cvref_t<Unit>, std::remove_cvref_t<Counit>>
constexpr auto	dedekind::category::make_adjunction (Left left, Right right, Unit unit, Counit counit)
	Factory for adjunction witnesses.
template<std::ranges::input_range R, typename T = std::ranges::range_value_t<R>, typename Op = std::plus<T>> requires IsMonoid<T, Op> && IsCopies<R> && HasCountingAction<T, Op>
constexpr T	dedekind::category::concat (R r, Op op={})
	concat on n copies of one value where the counts act in one step: \(x^n\) by the counting action, \(n \cdot x\) over a semimodule, x under an idempotent operation. The same signature as the binary method of :total and a stronger constraint, so resolution prefers it.
template<std::ranges::input_range R, std::semiregular M, typename H> requires std::invocable<const H&, M, std::ranges::range_value_t<R>>
constexpr M	dedekind::category::fold (R r, M v, H h)
	The fold along the walk: the standard's fold_left.
template<std::ranges::input_range R, std::semiregular M, typename H> requires IsCopies<R> && IsRightAction<H, M, std::ranges::range_value_t<R>>
constexpr M	dedekind::category::fold (R r, M v, H h)
	The fold under a monoid action of a sequence whose product has a fast form: v acted on once, by the product in the walk's order. The action law \(h(h(v, a), b) = h(v, a \cdot b)\) licenses this on any sequence, but it pays only where the product is cheaper than the actions one by one: elsewhere a product each costs more than an action each, a matrix by a matrix against a vector by a matrix. The fast form today is copies, whose product concat computes by squaring; periodic sequences are the natural next one. The same signature as the plain fold and a stronger constraint, so resolution prefers it.
template<std::regular S, std::semiregular Coalg>
constexpr unfold_view< S, Coalg >	dedekind::category::unfold (S seed, Coalg step)
	The unfold of seed by step.
template<std::regular X, std::semiregular Step>
constexpr chain_t< X, Step >	dedekind::category::chain (X x, Step step)
template<IsArrow End, IsArrow Step>
constexpr Until< End, Step >	dedekind::category::until (End end, Step step)
	The guard.
template<std::regular S, std::semiregular Coalg>
constexpr Unfold< S, Coalg >	dedekind::category::unfold (Coalg c)
	The anamorphism, as an arrow.
template<IsArrow Step> requires std::regular<Dom<Step>> && std::semiregular<Step>
constexpr Unfold< Dom< Step >, StepCoalgebra< Dom< Step >, Step > >	dedekind::category::chain (Step step)
	The chain of a partial step, as an arrow from the seeds: x >> chain(out) is chain(x, out).
template<std::regular S, std::semiregular Coalg, IsArrow F> requires std::same_as<Dom<F>, typename unfold_view<S, Coalg>::element_type>
constexpr unfold_view< S, Mapped< S, Coalg, F > >	dedekind::category::operator>> (const unfold_view< S, Coalg > &v, F f)
	ns >> f: f mapped over the walk, as a walk.
template<std::regular S, std::semiregular Coalg, IsArrow F> requires std::same_as<Dom<F>, typename unfold_view<S, Coalg>::element_type> && IsIdentityArrow<F>
constexpr unfold_view< S, Coalg >	dedekind::category::operator>> (const unfold_view< S, Coalg > &v, F)
	The functor's unit law, decided at the type: map id is the walk itself.
template<HasNNOStep C> requires std::totally_ordered<C>
constexpr Slice< C >	dedekind::category::slice (C lo, C hi)
template<HasNNOStep C, IsArrow F> requires std::totally_ordered<C> && std::same_as<Dom<F>, C>
constexpr unfold_view< std::optional< C >, detail_chain::SliceStep< C, F > >	dedekind::category::operator>> (const Slice< C > &s, F f)
	An arrow along a restricted chain: f(lo), ..., f(hi - 1), a range never built.
template<HasNNOStep N> requires std::regular<N>
constexpr auto	dedekind::category::chain ()
	The default chain of a carrier with the NNO's step, the one its certificate supplies: n >> chain<N>() is what Prior<N> reaches from n, n - 1, ..., 0 (the Jlt paper's Listing 3).
template<typename F>
constexpr auto	dedekind::category::exponential (F f)
	Internal Hom Factory (Exponential).
template<typename A, typename F>
constexpr auto	dedekind::category::exponential (F f)
template<typename A, typename B, typename F>
constexpr auto	dedekind::category::exponential (F f)
template<IsArrowFromProduct F>
constexpr auto	dedekind::category::curry (F f)
	Currying: (X × A → B) ⟹ (X → B^A).
template<IsArrow F> requires IsArrow<Cod<F>>
constexpr auto	dedekind::category::uncurry (F f)
	Uncurrying: (X → B^A) ⟹ (X × A → B).
template<typename T, typename Op> requires (!IsArrow<Op>) && std::regular_invocable<const Op&, const T&, const T&>
constexpr Curried< T, Op >	dedekind::category::curry (Op op)
	The operation curried.
template<typename T, typename Op>
constexpr Uncurried< T, Op >	dedekind::category::uncurry (Curried< T, Op > c)
	The inverse of curry<T>.
template<typename A, typename B>
constexpr auto	dedekind::category::ι_1 (A value)
	Left injection ι₁: A → A + B.
template<typename A, typename B>
constexpr auto	dedekind::category::ι_2 (B value)
	Right injection ι₂: B → A + B.
template<typename T, typename Op>
constexpr Sections< T, Op >	dedekind::category::operator>> (const Sections< T, Op > &f, const Sections< T, Op > &g)
	f >> g on sections: the identity absorbed, two sections one, \((b \mapsto a \cdot b) ; (c \mapsto a' \cdot c) = (b \mapsto (a' \cdot a) \cdot b)\) by associativity, which Sections asks of the operation, with no state, so that both sections are of one operation.
template<typename T, typename Op>
constexpr Arrows< T, Op >	dedekind::category::operator>> (const Morphisms< T, Op > &f, const Morphisms< T, Op > &g)
	f >> g on morphisms, into Arrows: the identity absorbed, two sections one, two pointers a composite.
template<typename T, typename Op>
constexpr Arrows< T, Op >	dedekind::category::operator>> (const Arrows< T, Op > &f, const Arrows< T, Op > &g)
	f >> g on arrows, restricted to one level: two morphisms compose as above, the identity is absorbed, and a composite of composites is refused.
template<IsArrow F, IsArrow G> requires std::same_as<Cod<F>, Cod<G>>
constexpr auto	dedekind::category::mediate_coproduct (F f, G g)
	Mediating morphism for Coproducts: [f, g]: (A + B) -> X.
template<typename F, typename A> requires IsExponential<F, A, std::invoke_result_t<F, A>>
constexpr auto	dedekind::category::eval (F f, A a)
	The canonical evaluation morphism for the CCC: (B^A × A) → B.
template<typename From, typename To>
constexpr To	dedekind::category::lift (From const &)
	Canonical lift From → To across the carrier lattice — discoverability alias dispatching to the registered bespoke arrow for (From, To).
template<typename A, typename B = A>
constexpr Flip< A, B >	dedekind::category::flip ()
template<IsArrow F, IsArrow G>
constexpr ProductArrow< F, G >	dedekind::category::product_arrow (const F &f, const G &g)
	f × g, built.
template<IsArrow F, IsArrow G>
constexpr SumArrow< F, G >	dedekind::category::sum_arrow (const F &f, const G &g)
	f + g, built.
template<IsArrow F, IsArrow G>
constexpr ProductArrow< F, G >	dedekind::category::operator* (const F &f, const G &g)
	f * g = f × g and f + g = f + g on arrows: the product and coproduct functors' action on arrows, as category theory writes them (Mac Lane, Awodey). A more specific overload keeps its own meaning: a set's * (its cartesian product, the classifier read through ∧), an additive hom-set's + (geometry's function spaces: the sum of parallel arrows, as in an additive category); the term grammar's * + act on terms, which are not arrows.
template<IsArrow F, IsArrow G>
constexpr SumArrow< F, G >	dedekind::category::operator+ (const F &f, const G &g)
template<typename F, typename G>
constexpr auto	dedekind::category::legs (const Pairing< F, G > &a)
	The legs of a former, for cata.
template<typename F, typename G>
constexpr auto	dedekind::category::legs (const Copairing< F, G > &a)
template<typename Epi, typename Section> requires IsSplitEpicPair<Epi, Section> && std::equality_comparable<Cod<Epi>>
constexpr bool	dedekind::category::split_epi_section_law_at (const Epi &epi, const Section &section, const Cod< Epi > &b)
	Law check for split epimorphisms at a concrete codomain element.
template<typename S, IsArrow E> requires IsSubobject<S, typename S::Domain> && std::same_as<Cod<E>, typename S::Domain> && std::equality_comparable< std::invoke_result_t<S const&, typename S::Domain const&>>
constexpr bool	dedekind::category::classifier_reindexing_definitional_witness_at (const S &s, const E &embedding, const Dom< E > &x)
	Definitional witness check for Axiom 7 reindexing through embedding.
template<typename A, typename Pred> requires IsSpecies<A> && std::invocable<std::decay_t<Pred>, const A&> && IsΩ<std::invoke_result_t<std::decay_t<Pred>, const A&>>
constexpr auto	dedekind::category::ambient_set (Pred predicate)
	Construct a set object over ambient species A from a characteristic predicate.
template<typename T, typename Hash, typename Equal, typename Alloc> requires IsSpecies<T>
constexpr auto	dedekind::category::ambient_set (std::unordered_set< T, Hash, Equal, Alloc > s)
	Lift std::unordered_set<T, ...> into an IsSet object, by value: the container is boxed, the lifted Subobject a value. (#607 slice 1, #1061).
template<typename T, typename Compare, typename Alloc> requires IsSpecies<T>
constexpr auto	dedekind::category::ambient_set (std::set< T, Compare, Alloc > s)
	Lift std::set<T, ...> into an IsSet object, by value: the container is boxed, the lifted Subobject a value. (#607 slice 1, #1061).
template<std::ranges::forward_range R> requires IsSpecies<std::ranges::range_value_t<R>> && (!requires(R& r, std::ranges::range_value_t<R> x) { r.contains(x); })
constexpr auto	dedekind::category::ambient_set (R r)
	Lift any std::ranges::input_range (a view, span, or container) into an IsSet object by wrapping std::ranges::find as the membership test. This is the Jlt-clean reading of a set — the set is its membership test — carried down to the std::ranges layer: a lazy view is a first-class IsSet, and it is constexpr where std::unordered_set (not constexpr-constructible with contents) is not. Excludes the keyed containers above by refusing a .contains() member, so those more specific overloads still win. The range is moved into the predicate (a view is cheap to own; the lifted Subobject carries its own copy). (#607 — the range slice of the wrapper-dissolution plan.).
template<typename T, IsArrow G> requires std::same_as<T, Dom<G>>
constexpr auto	dedekind::category::operator>> (Identity< T >, G g)
template<IsArrow F, typename T> requires std::same_as<Cod<F>, T>
constexpr auto	dedekind::category::operator>> (F f, Identity< T >)
template<typename T>
constexpr auto	dedekind::category::operator>> (Identity< T > i, Identity< T >)
template<typename L = Boole, typename Π, typename F_Raw, typename G_Raw>
constexpr auto	dedekind::category::pullback (F_Raw f_raw, G_Raw g_raw)
	The Pullback Factory — constructs the Fiber Product X ×_Z Y.
template<typename S> requires IsSubobject<std::remove_cvref_t<S>, typename std::remove_cvref_t<S>::Domain>
constexpr SubobjectInclusion< std::remove_cvref_t< S > >	dedekind::category::inclusion_arrow (const S &s)
template<typename S> requires IsSubobject<S, typename S::Domain>
constexpr ClassifierApex< S >	dedekind::category::as_classified (const S &s)

Variables
template<typename F>
constexpr bool	dedekind::category::is_functorial_v
template<typename F>
constexpr bool	dedekind::category::is_embedding_functor_v = false
	Trait registry for the IsEmbeddingFunctor concept.
template<typename F>
constexpr bool	dedekind::category::is_quotient_functor_v = false
	Trait registry for the IsQuotientFunctor concept.
template<typename T, typename Op>
constexpr bool	dedekind::category::is_periodic_v = is_periodic<T, Op>::value
template<typename T, typename Op>
constexpr bool	dedekind::category::is_saturating_v = is_saturating<T, Op>::value
template<typename T, typename Op>
constexpr bool	dedekind::category::is_exact_total_v = is_exact_total<T, Op>::value
template<typename T, typename Op>
constexpr bool	dedekind::category::is_total_by_construction_v
	Value form of is_total_by_construction.
template<typename T, typename Op>
constexpr bool	dedekind::category::is_total_v = is_total<T, Op>::value
	Value form of is_total.
template<typename T, typename Op>
constexpr bool	dedekind::category::is_cyclic_group_v = is_cyclic_group<T, Op>::value
	Shorthand access to the is_cyclic_group trait.
template<typename T, typename Op>
constexpr std::size_t	dedekind::category::cyclic_order_v = cyclic_order<T, Op>::value
template<typename T, typename Join, typename Meet, typename Not>
constexpr bool	dedekind::category::is_complemented_v = false
	Opt-in complement law: T carries a complement Not w.r.t. the bounded lattice (Join, Meet), i.e. \(a \vee \neg a = \top\) and \(a \wedge \neg a = \bot\) for every a.
template<typename Op, typename A, typename B>
constexpr bool	dedekind::category::is_closure_forcing_v = false
	Opt-in trait carrying the universal-property clause of IsClosureForcing — the engineer's honesty obligation that B is the canonical (smallest) carrier closing Op over A inputs. C++ concepts cannot quantify universally, so this part of the witness is asserted, not deduced. Pattern mirrors is_associative_v / is_saturating.
constexpr Projection< 0 >	dedekind::category::π {}
	The unary projection, the identity: the variable of a comprehension over one carrier.
constexpr Projection< 1 >	dedekind::category::π_1 {}
	The projections of a pair (and the first three of a tuple).
constexpr Projection< 2 >	dedekind::category::π_2 {}
constexpr Projection< 3 >	dedekind::category::π_3 {}
template<std::size_t K>
constexpr Projection< K >	dedekind::category::π_ {}
	The family: π_<k> is the k-th projection of a flat product.
constexpr Congruent	dedekind::category::is_even {2, 0}
	The even counts, the residue class of 0 modulo 2. Its reading on ℕ as a sequence, a path into the truth values, is dedekind::sequences::is_even (sequences:samples).
constexpr Pow2	dedekind::category::pow2 {}
	\(k \mapsto 2^k\) on std::size_t.
template<std::size_t W>
constexpr Pack< W >	dedekind::category::pack {}
	A pattern packed into the bit word of width W.
template<std::size_t W>
constexpr Unpack< W >	dedekind::category::unpack {}
	A machine word read back as a count.
constexpr std::size_t	dedekind::category::max_packed_width = 512
	The widest bit word the library precompiles: 512 bits, the widest common vector register, a std::bitset at every width above 64.
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_directed_v = is_directed<T, Rel>::value
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_codirected_v = is_codirected<T, Rel>::value
constexpr maybe_monad_tag	dedekind::category::maybe_monad {}
constexpr identity_monad_tag	dedekind::category::identity_monad {}
constexpr tuple_monad_tag	dedekind::category::tuple_monad {}
template<typename T, typename Op>
constexpr bool	dedekind::category::is_kleene_associative_v = false
template<typename T, typename Op>
constexpr bool	dedekind::category::is_kleene_commutative_v = false
template<typename T, typename Op>
constexpr bool	dedekind::category::is_kleene_invertible_v = false
template<typename T, typename Op>
constexpr T	dedekind::category::partial_unit_v = T{}
template<typename From, typename To>
constexpr bool	dedekind::category::lifts_to_v
	The dominance order: From ⊑ To iff the embedding species_embed<From, To> is registered. Reflexive and, over the shipped species, transitive (𝔹 ⊑ K₃ ⊑ Percent; 𝔹 ⊑ Chain<T>).
template<typename L>
constexpr bool	dedekind::category::logic_negation_is_involutive_v
	true iff the logic negation ¬ = L::RFL is a certified involution. Both shipped De Morgan logics (𝔹, K₃) qualify; a future intuitionistic species whose ¬¬ is only a closure would not. Downstream double-negation elimination gates on this so it stays honest per logic.
template<typename L>
constexpr bool	dedekind::category::logic_is_complemented_v = false
	true iff the species' reflection is a genuine complement (a∧¬a=⊥ and a∨¬a=⊤ for all a), i.e. the chain is 2-element. Boole qualifies; Kleene and Chain<T> (|Ω|>2) do not: their interior values have no complement. This is the logic_species=Boole reading of decidability: the clopen core Σ = 𝔹 ↪ Ω.
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_symmetric_v = is_symmetric<T, Rel>::value
	The "v" helper following the :species convention.
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_equality_v = is_equality<T, Rel>::value
constexpr detail_comprehension::CountingStage	dedekind::category::counting {}
	The stage counting what precedes it.
template<typename F, typename T>
constexpr bool	dedekind::category::is_involutive_v = is_involutive<F, T>::value
constexpr Reverse	dedekind::category::rev {}
	The reversal: of a word's positions, \(i \mapsto n - 1 - i\), the symmetry of a palindrome, and of a comparison.
template<typename M>
constexpr bool	dedekind::category::is_kleisli_deref_v = false
	is_kleisli_deref_v<M>: opt-in marker that the carrier's operator-> realises Kleisli dereference (for monadic carriers like Maybe<T>) or comonadic extract ε (for comonadic carriers like Identity<T>). Default false; specialise to true at the carrier site.
template<typename E, typename M>
constexpr bool	dedekind::category::is_kleisli_arrow_v = false
	User-declared "Kleisli arrow" witness (#380, step 1).
template<typename F, typename A, typename α>
constexpr bool	dedekind::category::is_initial_f_algebra_v = false
	Opt-in trait: does carrier A witness the initial F-algebra universal property for endofunctor F with structure map α?
template<typename F, typename A, typename α>
constexpr bool	dedekind::category::is_terminal_f_coalgebra_v = false
	Opt-in trait: does carrier A witness the terminal F-coalgebra universal property for endofunctor F with structure map α?
constexpr bool	dedekind::category::numeric_uses_builtin_overflow_checks = false
	Compile-time diagnostic: portable fallback overflow path enabled.
template<typename X, typename Ord>
constexpr bool	dedekind::category::is_lattice_bottom_for_v
template<typename X, typename Ord>
constexpr bool	dedekind::category::is_lattice_top_for_v = is_lattice_top_for<X, Ord>::value
template<typename X>
constexpr bool	dedekind::category::has_mixed_carrier_v = false
	Does the term X mix carriers anywhere — either two different known carriers, or a known carrier with an opaque (unknown) one? Only a uniform term fails this: all leaves opaque (the all-unknown case), or all leaves the same known carrier. A known/opaque mix counts as mixed because an opaque leaf carries no evidence it belongs to the known carrier's lattice. The structural laws use this to fail closed on any mixed term while still firing on the all-opaque case. (carrier_of reports void for both all-opaque and mixed, so a per-node is_void mismatch is what distinguishes a known/opaque boundary here.).
template<typename A>
constexpr bool	dedekind::category::has_mixed_carrier_v< Not< A > > = has_mixed_carrier_v<A>
template<typename A, typename B>
constexpr bool	dedekind::category::has_mixed_carrier_v< Meet< A, B > >
template<typename A, typename B>
constexpr bool	dedekind::category::has_mixed_carrier_v< Join< A, B > >
template<typename X>
constexpr bool	dedekind::category::idempotent_leaf_v
	Is X a leaf whose VALUE is determined by its TYPE? Idempotence X∧X=X is sound only for such a leaf. Two same-type instances are then necessarily the same set, so collapsing them is correct. The default is std::is_empty_v<X>, true for a stateless tag or an NTTP-encoded carrier. A carrier with RUNTIME-STATEFUL leaves specialises this to false for them. sets does so for Set<T,L,P> whose predicate P carries a runtime field (e.g. a Point's pivot). The type-based idempotence then does not collapse two distinct-but-same-type values.
template<typename Elem, typename Node>
constexpr bool	dedekind::category::is_join_containing_v = false
	Is Elem one of the operands of the Join node Node?
template<typename Elem, typename A, typename B>
constexpr bool	dedekind::category::is_join_containing_v< Elem, Join< A, B > >
template<typename Elem, typename Node>
constexpr bool	dedekind::category::is_meet_containing_v = false
	Is Elem one of the operands of the Meet node Node?
template<typename Elem, typename A, typename B>
constexpr bool	dedekind::category::is_meet_containing_v< Elem, Meet< A, B > >
template<typename X>
constexpr bool	dedekind::category::is_join_node_v = false
	Is X a Join node?
template<typename A, typename B>
constexpr bool	dedekind::category::is_join_node_v< Join< A, B > > = true
template<typename T, typename Ord>
constexpr bool	dedekind::category::is_distributive_lattice_for_v
	Is the lattice (carrier T, order Ord) distributive? Keyed to the order like the boundedness markers. The canonical (std::less_equal chain) case derives from the concept gates IsLatticeCategory<T> && IsOrderDistributiveLatticeOperations<T> — so a carrier that is not a lattice under std::less_equal is not licensed to distribute (NB the bare distributive<T>(max{}, min{}) trait is unconditionally true, which would license any carrier — hence the concept gate). A NON-chain distributive lattice (a custom Ord) opts in by specialising this to true (the Jlt assertion — the same posture as the injected total order). A canonical chain is gated distributive but never actually distributes: its joins glb/lub-collapse first.
template<typename X>
constexpr bool	dedekind::category::is_not_node_v = false
	Is X a Not node?
template<typename A>
constexpr bool	dedekind::category::is_not_node_v< Not< A > > = true
template<typename X>
constexpr bool	dedekind::category::is_meet_node_v = false
	Is X a Meet node?
template<typename A, typename B>
constexpr bool	dedekind::category::is_meet_node_v< Meet< A, B > > = true
template<typename T>
constexpr bool	dedekind::category::is_lattice_node_v
	Whether T is one of the nodes, Meet, Join or Not.
template<typename T, typename Ord>
constexpr bool	dedekind::category::is_de_morgan_negation_for_v = false
	Does the lattice (carrier T, order Ord) carry an involutive order-reversing negation (¬¬a=a and the De Morgan laws)? Keyed to the order and opt-in (default false — the Jlt assertion), the same posture as is_distributive_lattice_for_v.
template<>
constexpr bool	dedekind::category::is_de_morgan_negation_for_v< bool, canonical_order > = true
	Canonical bool is a De Morgan (indeed Boolean) algebra: ¬ is std::logical_not, involutive with the De Morgan laws — the production carrier that activates the negation laws (the all-laws-fire oracle).
template<typename T, typename Ord>
constexpr bool	dedekind::category::is_complemented_lattice_for_v = false
	Does the lattice (carrier T, order Ord) carry a genuine complement (a∧¬a=⊥, a∨¬a=⊤), not merely a De Morgan negation? Keyed to the order and opt-in (default false). A complemented lattice is also a De Morgan algebra, so a carrier asserting this should also assert is_de_morgan_negation_for_v.
template<>
constexpr bool	dedekind::category::is_complemented_lattice_for_v< bool, canonical_order >
	Canonical bool is a Boolean (hence complemented) lattice.
template<typename RA, typename RB>
constexpr bool	dedekind::category::is_complement_pair_v
	Are RA and RB a complement pair (RB=¬RA or RA=¬RB)?
template<typename Not, typename T, typename Rel, typename Join, typename Meet>
constexpr bool	dedekind::category::is_complement_v
template<typename T>
constexpr bool	dedekind::category::has_one_value_v
template<typename F, typename G>
constexpr bool	dedekind::category::commutes_v
template<typename F>
constexpr bool	dedekind::category::is_self_inverse_v = is_self_inverse<F>::value
template<typename E>
constexpr bool	dedekind::category::is_monic_arrow_v = false
	User-declared monicity witness for an arrow type.
template<typename E>
constexpr bool	dedekind::category::is_constant_arrow_v = false
	The constancy of an arrow: declared for ConstantMorphism (:discrete), read off composition by the law engine (:posetal).
template<typename E>
constexpr bool	dedekind::category::is_epic_arrow_v = false
	User-declared epicity witness for an arrow type.
template<typename F, typename T, typename Op, typename Op2 = Op>
constexpr bool	dedekind::category::is_homomorphism_v = is_homomorphism<F, T, Op, Op2>::value
	Value form of is_homomorphism.
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_reflexive_v = is_reflexive<T, Rel>::value
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_transitive_v = is_transitive<T, Rel>::value
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_antisymmetric_v = is_antisymmetric<T, Rel>::value
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_connex_v = is_connex<T, Rel>::value
template<typename T, typename Op>
constexpr bool	dedekind::category::is_associative_v = is_associative<T, Op>::value
template<typename T, typename Op>
constexpr bool	dedekind::category::is_commutative_v = is_commutative<T, Op>::value
template<typename T, typename Op>
constexpr bool	dedekind::category::is_idempotent_v = is_idempotent<T, Op>::value
	Helper for shorthand access in concepts.
template<typename T>
constexpr size_t	dedekind::category::characteristic_v
	The Characteristic of the Species.
template<typename T, typename Mult, typename Add>
constexpr bool	dedekind::category::is_distributive_v = false
	Trait to mark the structural glue between two operators. axiom: a * (b + c) = (a * b) + (a * c).
template<typename T, typename Op>
constexpr bool	dedekind::category::is_invertible_v = inverse_trait<T, Op>::exists
	The Shorthand for the Registry.
template<typename T>
constexpr bool	dedekind::category::is_transfinite_v = is_transfinite<T>::value
	Shorthand helper.
template<typename T, typename Op1, typename Op2>
constexpr bool	dedekind::category::is_absorptive_v = false
	The Absorber Trait (Axiom: a ∨ (a ∧ b) = a). Represents the structural tethering between two dual operations.
template<typename F, typename Op = std::less_equal<>>
constexpr bool	dedekind::category::is_monotone_v
template<typename F, typename Op = std::less_equal<>>
constexpr bool	dedekind::category::is_antimonotone_v
constexpr std::array< ArrowLaw, 6 >	dedekind::category::every_arrow_law
template<typename F, typename Op = std::less_equal<>>
constexpr ArrowLaws	dedekind::category::arrow_laws_v = declared_arrow_laws<F, Op>()
template<typename F, typename G, typename Op = std::less_equal<>>
constexpr bool	dedekind::category::is_adjoint_v = is_adjoint<F, G, Op>::value
template<typename M, typename S, typename AddM, typename AddS, typename MultS, typename Act>
constexpr bool	dedekind::category::is_linear_action_v
	Value form of is_linear_action.
template<typename R>
constexpr bool	dedekind::category::is_left_total_v = false
	User-declared left-totality witness for a binary relation.
template<typename R>
constexpr bool	dedekind::category::is_right_unique_v = false
	User-declared right-uniqueness witness for a binary relation.
template<typename R>
constexpr bool	dedekind::category::is_left_unique_v = false
	Left-uniqueness (injectivity of the relation): each b ∈ B is related to at most one a; R° right-unique. Same opt-in pattern; derived for the relational nodes by the rule table (relational:dyadic, Laws).
template<typename R>
constexpr bool	dedekind::category::is_right_total_v = false
	Right-totality (surjectivity of the relation): every b ∈ B is related to some a; R° left-total. Same opt-in pattern, derived likewise. With the other three: an isomorphism of Rel.
template<typename R, typename T, typename Op>
constexpr bool	dedekind::category::is_congruence_v = false
	User-declared congruence witness: R respects Op on T.
template<typename Seq, typename Idx>
constexpr bool	dedekind::category::is_eval_arrow_v = false
	is_eval_arrow_v<Seq, Idx>: opt-in marker that the carrier's operator[] realises the CCC eval counit. Default false; specialise to true at the carrier site (FinitePath<T>, Vec2V<T>, …) when the subscript-as-eval reading holds.
template<typename E>
constexpr bool	dedekind::category::is_regular_epi_v = false
	User-declared witness: E is a regular epi (the coequalizer of some parallel pair).
template<typename M>
constexpr bool	dedekind::category::is_regular_mono_v = false
	User-declared witness: M is a regular mono (the equalizer of some parallel pair). Dual to is_regular_epi_v.
template<typename C>
constexpr bool	dedekind::category::is_factorisation_system_v = false
	User-declared witness: category C admits a (regular epi, mono) factorisation system — every arrow f of C factors as f = m ∘ e with e a regular epi and m a mono, uniquely up to iso.
template<typename C>
constexpr bool	dedekind::category::is_regular_category_v = false
	User-declared witness: C is a regular category — has finite limits, kernel pairs and coequalizers of kernel pairs, and regular epis are stable under pullback.
template<typename C>
constexpr bool	dedekind::category::is_exact_category_v = false
	User-declared witness: C is an exact category — a regular category in which every equivalence relation is the kernel pair of some arrow (every equivalence relation is effective).

reduce_β for a Compose node — the canonical β exhibit
reduce_β is the β (F-algebra structure map, i.e. the one-step β-reduction) that cata applies after folding a node's legs. This overload set is the canonical exhibit: the reducer's first law, the monoid law of composition, co-located with the cata engine. The identity is the unit (id∘f = f = f∘id), so an Identity in a reduced leg is dropped. Dispatch is structural on Identity<T> in the reduced leg (no is-identity tag): the overloads pattern-match the leg types, and partial ordering picks the Identity ones over the generic IsArrow one. The first parameter is the Compose node as a type-tag for β dispatch (which constructor is this?); its own legs are unused — cata passes the already-reduced legs rf / rg, which is what β combines. Found by ADL, so a partition MAY instead scatter its node's reduce_β next to that node's vocabulary; the composition law lives here as the reference instance.
template<IsArrow F, IsArrow G, IsArrow RF, IsArrow RG>
constexpr auto	dedekind::category::reduce_β (const Compose< F, G > &, const RF &rf, const RG &rg)
template<IsArrow F, IsArrow G, typename T, IsArrow RG>
constexpr RG	dedekind::category::reduce_β (const Compose< F, G > &, const Identity< T > &, const RG &rg)
template<IsArrow F, IsArrow G, IsArrow RF, typename T>
constexpr RF	dedekind::category::reduce_β (const Compose< F, G > &, const RF &rf, const Identity< T > &)
template<IsArrow F, IsArrow G, typename T, typename U>
constexpr Identity< T >	dedekind::category::reduce_β (const Compose< F, G > &, const Identity< T > &i, const Identity< U > &)
template<typename F, typename G, typename RF, typename RG>
constexpr auto	dedekind::category::reduce_β (const Pairing< F, G > &, const RF &rf, const RG &rg)
	A pairing (copairing) rebuilt from its reduced legs: inert.
template<typename F, typename G, typename RF, typename RG>
constexpr auto	dedekind::category::reduce_β (const Copairing< F, G > &, const RF &rf, const RG &rg)

The legs of a node, for @c cata (@c :f_algebra)
The term functor stated once per node: the operands, by reference.
template<typename A, typename B>
constexpr auto	dedekind::category::legs (const Meet< A, B > &m)
template<typename A, typename B>
constexpr auto	dedekind::category::legs (const Join< A, B > &j)
template<typename A>
constexpr auto	dedekind::category::legs (const Not< A > &n)

Files
file	src/main/modules/dedekind/category/category.cppm
	Level 0–4: categorical bedrock + ETCS facade.
file	src/main/modules/dedekind/category/action.cppm
	The Morphisms of Influence (Actions and Representations).
file	src/main/modules/dedekind/category/adjunction.cppm
	Adjoint functors (the Free / Forgetful axis).
file	src/main/modules/dedekind/category/automaton.cppm
	The matcher of a set of words of one length, specialised to it: the minimal automaton of \(\Sigma^* L\), a value computed by one constexpr function at either binding time.
file	src/main/modules/dedekind/category/cartesian.cppm
	Cartesian Closed Category (CCC) Foundations.
file	src/main/modules/dedekind/category/cartesian_bicategory.cppm
	The meet is the right adjoint of the diagonal (Δ⊣∧), reified.
file	src/main/modules/dedekind/category/chain.cppm
	Dedekind's chain as a range: the unfold of a seed by a coalgebra, the chain of a step guarded by an end, the arrow mapped along it, the bounded chain [lo, hi], and the default chain of a carrier with the NNO's step (the Jlt paper's Figure 2 and Listing 3, #981). The NNO itself, its step and Lambek's destructor Prior, are :nno's; the folds over a chain are :total's concat and :action's fold.
file	src/main/modules/dedekind/category/comprehension.cppm
	Monad comprehensions over a finite chain: the queries of SQL and LINQ, where, select, order_by and take, and the folds that end them.
file	src/main/modules/dedekind/category/concrete.cppm
	Concrete categories: faithful U : 𝒞 → Set, sub-object machinery, lattice operations on χ-classified sets.
file	src/main/modules/dedekind/category/discrete.cppm
	The Discrete Infrastructure (Points as Arrows).
file	src/main/modules/dedekind/category/equivalence.cppm
	Equivalence relations: reflexive + symmetric + transitive predicates, composing the existing axiom traits in :species with a new symmetry trait.
file	src/main/modules/dedekind/category/etcs.cppm
	Elementary Theory of the Category of Sets (ETCS) facade.
file	src/main/modules/dedekind/category/f_algebra.cppm
	Initial F-algebras and terminal F-coalgebras.
file	src/main/modules/dedekind/category/factorisation.cppm
	(Regular epi, mono) factorisation system theory — the categorical context for the image-as-coequalizer-of-kernel-pair theorem narrated in :image (#718 Slice 1).
file	src/main/modules/dedekind/category/filtered.cppm
	Filtered categories — categories whose finite diagrams have a cocone.
file	src/main/modules/dedekind/category/functor.cppm
	The Functorial Spine (Structure Preservation).
file	src/main/modules/dedekind/category/image.cppm
	Image-as-coequalizer-of-kernel-pair: IsImageOf<S, F> on the mono side and IsCoequalizer<Q, F, G> on the quotient side.
file	src/main/modules/dedekind/category/involution.cppm
	Involution — a direction-reversal that is its own inverse — the atomic shape behind the dagger of a \(\dagger\)-category.
file	src/main/modules/dedekind/category/iso.cppm
	The retract / iso-enabling arrow surface: the constructions that turn a factorisation class into a downstream decidability class.
file	src/main/modules/dedekind/category/kleisli.cppm
	The Kleisli Partition (The Extension Systems).
file	src/main/modules/dedekind/category/lattice.cppm
	Lattice categories — the Form-chain row 4 (#698).
file	src/main/modules/dedekind/category/lattice_term.cppm
	The assembled lattice-law term reducer: the normal form of a term over a bounded lattice, built from the induced laws in :lattice, as one algebra for cata, its type at compile time and its value at run time.
file	src/main/modules/dedekind/category/limit.cppm
	Universal Limits: boundary objects (Initial and Terminal) and binary products.
file	src/main/modules/dedekind/category/logic.cppm
	The Rules of Thought (Ω).
file	src/main/modules/dedekind/category/mereology.cppm
	Embryonic Mereology (Part-Whole and Skew Algebraic Core).
file	src/main/modules/dedekind/category/monad.cppm
	Monads and Comonads (Context as Algebra).
file	src/main/modules/dedekind/category/morphism.cppm
	The Skeletal Morphism (Structural Cement).
file	src/main/modules/dedekind/category/natural.cppm
	Natural Transformations (The Slide between Functors).
file	src/main/modules/dedekind/category/nno.cppm
	The Natural Numbers Object — Lawvere's ETCS Axiom 9 — and the upstream home of Peano recursion / primitive recursion / the Peano successor (categorical idiom + textbook synonyms below).
file	src/main/modules/dedekind/category/numeric.cppm
	The Numeric Landing (IEEE 754 and Lipschitz Boundaries).
file	src/main/modules/dedekind/category/partial.cppm
	The Logic of Potentiality (Partial Algebra).
file	src/main/modules/dedekind/category/periodic.cppm
	Periodic arrows on the counts and the counts they license: an arrow f is periodic with period p when \(f(k + p) = f(k)\), a law declared at a generator and inferred at a composite, so that a count along a chain of any length is (n div p) periods and a remainder (the Jlt paper's tensor exhibit, #1104).
file	src/main/modules/dedekind/category/posetal.cppm
	Posetal categories — categories derived from partial orders.
file	src/main/modules/dedekind/category/pullback.cppm
	Limits — Equalizers and Fiber Products (Pullbacks).
file	src/main/modules/dedekind/category/runs.cppm
	Run lists over a finite chain: a subset of \([0, n)\) as the positions where its membership changes, the canonical form of a decidable set on a chain, bounded by its type and on the stack.
file	src/main/modules/dedekind/category/small.cppm
	Small Categories (Enumerated Morphism Sets).
file	src/main/modules/dedekind/category/species.cppm
	The Reified Machine (The Taxonomic Bricks).
file	src/main/modules/dedekind/category/thin.cppm
	Thin categories — categories whose hom-sets contain at most one morphism.
file	src/main/modules/dedekind/category/topoi.cppm
	The Internal Logic of the Topos.
file	src/main/modules/dedekind/category/total.cppm
	The Laws of Total Algebra (The Algebraic Hierarchy).