module Vector where open import Nat data Vect (A : Set) : Nat → Set where [] : Vect A zero _::_ : {n : Nat} → A -> Vect A n -> Vect A (succ n) head : {A : Set} → {n : Nat} → Vect A (succ n) -> A head (a :: as) = {!!}