```{- SSGIP Examples, Stephanie Weirich, March 24-26, 2010 -}
{-# OPTIONS --type-in-type --no-termination-check #-}
module ssgip.main where
open import Data.Unit
open import Data.Sum hiding (map)
open import Data.Nat
open import Data.List hiding (map; zipWith; replicate)
open import Data.Product hiding (map)
open import Relation.Binary.PropositionalEquality

infixl 50 _⊛_
infixl 50 _<>_

data Bool : Set where
true   : Bool
false  : Bool

_∧_ : Bool → Bool → Bool
true  ∧ true  = true
_     ∧ _     = false

if_then_else : ∀ { A } → Bool → A → A → A
if  true   then e1 else e2  = e1
if  false  then e1 else e2  = e2

replicate : ∀ {A} → ℕ → A → List A
replicate zero     x  = []
replicate (suc n)  x  = (x ∷ replicate n x)

replicate-spec : ∀ {A} → (x : A) → (n : ℕ)
→ length (replicate n x) ≡ n
replicate-spec x zero = refl
replicate-spec x (suc n) with replicate-spec x n
... | pf = cong suc pf

data Vec (A : Set) : ℕ → Set where
[]   : Vec A zero
_∷_  : ∀ {n} → A → Vec A n → Vec A (suc n)

repeat : ∀ {A} → (n : ℕ) → A → Vec A n
repeat zero     x = []
repeat (suc n)  x = x ∷ repeat n x

postulate error : ∀ {A} → A

_<>_  : ∀ {A B} → List (A → B) → List A → List B
[]        <> []        = []
(a ∷ As)  <> (b ∷ Bs)  = (a b ∷ As <> Bs)
_         <> _         = error

_⊛_  : ∀ {A B n} → Vec (A → B) n → Vec A n → Vec B n
[]        ⊛ []        = []
(a ∷ As)  ⊛ (b ∷ Bs)  = (a b ∷ As ⊛ Bs)

zerox        : (Bool → Bool) → Bool → Bool
zerox   f x  = x

onex         : (Bool → Bool) → Bool → Bool
onex    f x  = f x

twox         : (Bool → Bool) → Bool → Bool
twox    f x  = f (f x)
nx  : ℕ → (Bool → Bool) → Bool → Bool
nx zero     f  x  = x
nx (suc n)  f  x  = nx n f (f x)

app-nat       : (ℕ → ℕ) → ℕ → ℕ
app-nat f x   = f x

app-bool      : (Bool → Bool) → Bool → Bool
app-bool f x  = f x
app : ∀ {A} → (A → A) → A → A
app f x = f x

eq-nat : ℕ → ℕ → Bool
eq-nat zero     zero     = true
eq-nat (suc n)  (suc m)  = eq-nat n m
eq-nat _        _        = false

eq-bool : Bool → Bool → Bool
eq-bool false   false    = true
eq-bool true    true     = true
eq-bool _       _        = false

⟦_⟧ : Bool → Set
⟦ b ⟧ = if b then ℕ else Bool

eq-nat-bool : (b : Bool) → ⟦ b ⟧ → ⟦ b ⟧ → Bool
eq-nat-bool true  = eq-nat
eq-nat-bool false = eq-bool

data Type : Set where
nat   : Type
bool  : Type
pair  : Type → Type → Type

zeroApp   : ∀ {A B} → B → A → B
zeroApp   f x   = f

oneApp    : ∀ {A B} → (A → B) → A → B
oneApp    f x   = f x

twoApp    : ∀ {A B} → (A → A → B) → A → B
twoApp    f x   = f x x

NAPP : ℕ → Set → Set → Set
NAPP zero     A B = B
NAPP (suc n)  A B = A → NAPP n A B

nApp : ∀ {A B} → (n : ℕ) → NAPP n A B → A → B
nApp zero     f x  = f
nApp (suc n)  f x  = nApp n (f x) x

f : (b : Bool) → if b then ℕ else Bool
f true = 0
f false = false

anything : ∀ {A} → A
anything = anything

head : ∀ {A n} → Vec A (suc n) → A
head ( x ∷ xs ) = x
```