http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.TypesSummerSchool2007

Fin.agda

module Fin where

data Fin : ℕ → Set where
  fzero : {n : ℕ} → Fin (succ n)
  fsuc  : {n : ℕ} → Fin n → Fin (succ n)

data ⊥ : Set where

empty : Fin zero → ⊥
empty ()

_!_ : {A : Set}{n : ℕ} → Vec A n → Fin n → A
ε ! fzero = empty
(x ▶ xs) ! fzero = x
(x ▶ xs) ! (fsuc n) = xs ! n

tabulate : {A : Set}{n : ℕ} → (Fin n → A) → Vec A n
tabulate f fzero = ε
tabulate f (fsuc n) = f fzero ▶ tabulate f n

List.agda

module List where

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

infixl 10 _∷_

map : {A B : Set} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

_++_ : {A : Set} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

data All {A : Set}{P : A → Set} : List A → Set where
  [] : All P []
  _∷_ : ∀ {x xs} (px : P x) (pxs : All P xs) → All P (x ∷ xs)

data Some {A : Set}{P : A → Set} : List A → Set where
  here  : ∀ {x xs} (px : P x) → Some P (x ∷ xs)
  there : ∀ {x xs} (pxs : Some P xs) → Some P (x ∷ xs)

_∈_ : {A : Set} → List A → Set
x ∈ xs = Some (here x) xs

--

Nat.agda

module Nat where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

infixl 60 _+_
infixl 70 _*_

_+_ : ℕ → ℕ → ℕ
n + zero = n
n + succ m = succ (n + m)

_*_ : ℕ → ℕ → ℕ
n * zero = zero
n * succ m = n * m + n

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

assoc : ∀{x y z : ℕ} → x + (y + z) == (x + y) + z
assoc {zero} {y} {z} = refl
assoc {succ x} {y} {z} = refl (assoc {x} {y} {z}) 

Vec.agda

module Vec where

data Vec (A : Set) : ℕ → Set where
  ε : Vec A zero
  _▶_ : {n : ℕ} → A → Vec A n → Vec A (succ n)

vec : {A : Set}{n : ℕ} → A → Vec A n
vec zero _ = ε
vec (succ n) e = e ▶ vec n e

infixl 4 _<*>_

_<*>_ : {A B : Set}{n : ℕ} → Vec (A → B) n → Vec A n → Vec B n
ε <*> ε = ε
(f ▶ fs) <*> (e ▶ es) = (f e) ▶ (fs <*> es) 

map : {A B : Set}{n : ℕ} → (A → B) → Vec A n → Vec B n
map f v = (vec f) <*> v

zip : {A B C : Set}{n : ℕ} → (A → B → C) → Vec A n → Vec B n → Vec C n
zip f xs ys = (vec f) <*> xs <*> ys