Martin Escardo 2011.

\begin{code}

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

module Sequence where

open import Naturals
open import NaturalsAddition
open import SpartanMLTT hiding (_+_)

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


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


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


hd-tl-eta : {X :   U} {α : (n : )  X n}  (hd α ∶∶ tl α)  α
hd-tl-eta {X} = funext {} {X} lemma
 where 
  open import FunExt
  lemma : {α : (n : )  X n}  (i : )  (hd α ∶∶ tl α) i  α i
  lemma 0 = refl
  lemma (succ i) = refl


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


open import Retraction

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

\end{code}

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

\begin{code}

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

\end{code}