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



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

rightShiftedSequences(x) y:ST(y)=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 SS has a right shift operator for every term s:Ss:S,

s:ST s 1:(S)(S)s:S \vdash T^{-1}_s:(\mathbb{N} \to S) \to (\mathbb{N} \to S)

defined as

T s 1(x)(0)=sT^{-1}_s(x)(0) = s
T s 1(x)(i+i)x(i)T^{-1}_s(x)(i + i) \coloneqq x(i)

for i: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.