data Bool : Set where
  true : Bool
  false : Bool

flip : Bool → Bool
flip true = false
flip false = true

_&&_ : Bool → Bool → Bool
true && true = true
_ && _ = false

if_then_else_ : Bool → Bool → Bool → Bool
if true then x else y = x
if false then x else y = y

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

{-# BUILTIN NATURAL Nat #-}

five : Nat
five = 5

_+_ : Nat → Nat → Nat
zero + b = b
suc a + b = suc (a + b)

+2 : Nat → Nat
+2 n = suc (suc n)

data List (A : Set) : Set where
  nil : List A
  cons : A → List A → List A

append : ∀ {A : Set} → List A → List A → List A
append nil ys = ys
append (cons x xs) ys
  = cons x (append xs ys)

head : ∀ {A : Set} → List A → A
head nil = {!!}
head (cons x l) = x
-- List : Set → Set

foo : List Nat
foo = cons 5 (cons 2 nil)

cop : Bool → Set
cop true = Nat
cop false = Bool

d : cop true
d = 5

e : cop false
e = false

data Vec (A : Set) : Nat → Set where
  [] : Vec A 0

  _∷_ : ∀ {n : Nat} →
    A → Vec A n → Vec A (suc n)

v : Vec Nat 3
v = 5 ∷ (4 ∷ (3 ∷ []))

_++_ : ∀ {A : Set} {n m : Nat} →
  Vec A n → Vec A m → Vec A (n + m)
[] ++ w = w
(x ∷ v) ++ w = x ∷ (v ++ w)

headv : ∀ {A : Set} {n : Nat} →
        Vec A (suc n) → A
headv (x ∷ v) = x

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ {a : A} → a ≡ a

simple : 4 ≡ (2 + 2)
simple = refl

sym : ∀ {A : Set} {x y : A} →
      x ≡ y → y ≡ x
sym refl = refl

trans : ∀ {A : Set} {x y z : A} →
        x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

cong : ∀ {A B : Set} {x y : A}
       (f : A → B) → x ≡ y → (f x) ≡ (f y)
cong f refl = refl

+-zero : ∀ (n : Nat) → n ≡ (n + zero)
+-zero zero = refl
+-zero (suc n) = cong suc (+-zero n)

+-suc : ∀ (n m : Nat) →
  suc (n + m) ≡ (n + suc m)
+-suc zero m = refl
+-suc (suc n) m = cong suc (+-suc n m)
-- +-suc n m : suc (n + m) ≡ (n + suc m)

+-comm : ∀ (n m : Nat) → (n + m) ≡ (m + n)
+-comm zero m = +-zero m
+-comm (suc n) m
  = trans (cong suc (+-comm n m))
          (+-suc m n)
-- +-comm n m : n + m ≡ m + n
-- suc (n + m) ≡ suc (m + n) ≡ (m + suc n)