FinVector-cons.agda

module FinVector-cons (T : Set) where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data Fin : Nat → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

postulate
  funext : {A B : Set} → {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

B : Nat → Set
B n = Fin n → T

cons : ∀ {n} (t : T) → B n → B (suc n)
cons x xs zero = x
cons x xs (suc z) = xs z

head : ∀ {n} → B (suc n) → T
head xs = xs zero

tail : ∀ {n} → B (suc n) → B n
tail xs n = xs (suc n)


cons-ok : ∀ {n} → (b : B (suc n)) → ∀ n → cons (head b) (tail b) n ≡ b n
cons-ok b zero = refl
cons-ok b (suc n) = refl

cons-ok-ext : ∀ {n} → (b : B (suc n)) → cons (head b) (tail b) ≡ b
cons-ok-ext b = funext (cons-ok b)