[[!redirects right shift operators]] #Contents# * table of contents {:toc} ## 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$: $$\mathrm{rightShiftedSequences}(x) \coloneqq \sum_{y:\mathbb{N} \to S} T(y) = 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$, $$s:S \vdash T^{-1}_s:(\mathbb{N} \to S) \to (\mathbb{N} \to S)$$ defined as $$T^{-1}_s(x)(0) = s$$ $$T^{-1}_s(x)(i + i) \coloneqq x(i)$$ for $i:\mathbb{N}$. ## See also ## * [[sequence]] * [[left shift operator]] * [[sequential antiderivative]] category: not redirected to nlab yet