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

Showing changes from revision #2 to #3: Added | Removed | Changed

# 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}$.