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). More...

Concept definition

template<typename F>

concept dedekind::category::IsFiniteChainSequence = IsArrow<F> && IsCountWord<Dom<F>>

dedekind::category::IsArrow

A type that knows its own Domain (A) and Codomain (B), objects it maps between: called at the domain'...

Definition morphism.cppm:168

dedekind::category::IsCountWord

A word of the counts: an integer chain whose arithmetic wraps at its cyclic order,...

Definition chain.cppm:62

dedekind::category::IsFiniteChainSequence

A sequence on finite chains: an arrow out of the counts, read along a chain of them (the Jlt paper's ...

Definition chain.cppm:458

Detailed Description

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).

Template Parameters

F	the arrow.