Martin Escardo 2011.

\begin{code}

{-# OPTIONS --without-K #-}

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 {X} = funext {ℕ} {X} 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 Retraction
open import CurryHoward

cons-retraction : {X : ℕ → Set} → retraction(cons{X})
cons-retraction α = ∃-intro (hd α , tl α) hd-tl-eta

\end{code}

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

\begin{code}

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

\end{code}