Contents

Definition

Given a type $S$ and a sequence $x:\mathbb{N} \to S$, the type of right shifted sequences of $x$ is the fiber of the left shift operator at $x$:

A right shift operator is a term of the above type.

Every sequence in $S$ has a right shift operator for every term $s:S$,

defined as

for $i:\mathbb{N}$.

See also

• sequence
• left shift operator
• sequential antiderivative