Martin Escardo 2011.

\begin{code}

module Sequence where

open import Naturals
open import Equality

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


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


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


hd-tl-eta : {X :   Set} 

  {α : (n : )  X n}  ((hd α) ∶∶ (tl α))  α

hd-tl-eta = extensionality lemma
 where 
  open import Extensionality

  lemma :  {α}   i  ((hd α) ∶∶ (tl α)) i  α i
  lemma 0 = refl
  lemma (succ i) = refl


open import SetsAndFunctions hiding (_+_)

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


open import Surjection
open import CurryHoward

cons-surjection : {X :   Set}  

 surjective(cons{X})

cons-surjection α = ∃-intro (hd α , tl α) hd-tl-eta 

\end{code}

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

\begin{code}

open import Addition

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

\end{code}