#
Homotopy Type Theory
right shift operator > history (Rev #2)

# 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

Revision on June 15, 2022 at 22:59:21 by
Anonymous?.
See the history of this page for a list of all contributions to it.