#
Homotopy Type Theory
right shift operator > history (changes)

Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

~~
~~# 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$:

~~
~~$\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

~~
~~~~
~~
Last revised on June 17, 2022 at 18:57:07.
See the history of this page for a list of all contributions to it.