Martin Escardo 2011.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-} 

open import UF-FunExt

module Sequence (fe :  {U V}  funext U V) where

open import SpartanMLTT hiding (_+_)
open import UF-Retracts
open import NaturalsAddition

_∶∶_ :  {U} {X :   U ̇}  X 0  ((n : )  X(succ n))  ((n : )  X n)
(x ∶∶ α) 0 = x
(x ∶∶ α) (succ n) = α n


hd :  {U} {X :   U ̇}  ((n : )  X n)  X 0
hd α = α 0


tl :  {U} {X :   U ̇}  ((n : )  X n)  ((n : )  X(succ n))
tl α n = α(succ n)


hd-tl-eta :  {U} {X :   U ̇} {α : (n : )  X n}  (hd α ∶∶ tl α)  α
hd-tl-eta {U} {X} = dfunext fe lemma
 where 
  lemma : {α : (n : )  X n}  (i : )  (hd α ∶∶ tl α) i  α i
  lemma 0 = refl
  lemma (succ i) = refl


cons :  {U} {X :   U ̇}  X 0 × ((n : )  X(succ n))  ((n : )  X n)
cons(x , α) = x ∶∶ α

cons-retraction :  {U} {X :   U ̇}  retraction(cons {U} {X})
cons-retraction α = (hd α , tl α) , hd-tl-eta 

\end{code}

(In fact it is an isomorphism, but I won't bother.)

\begin{code}

tail :  {U} {X :   U ̇}  (n : )  ((i : )  X i)  ((i : )  X(i + n))
tail n α i = α(i + n)

\end{code}