Tutorial scratchpad for Dependently Typed Programming in Agda

Tutorial.agda

module Tutorial where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

{-# BUILTIN NATURAL Nat  #-}

infix 3 _+_
_+_ : Nat -> Nat -> Nat
zero + m = m
suc n + m = suc (n + m)

data False : Set where
record True : Set where

data Bool : Set where
  true false : Bool

data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A
infixr 40 _::_

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

infix 50 _++_
_++_ : {A : Set} -> List A -> List A -> List A
[] ++ ys = ys
(x :: xs) ++ ys = x :: xs ++ ys

data Fin : Nat -> Set where
  fzero : {n : Nat} -> Fin (suc n)
  fsuc : {n : Nat} -> Fin n -> Fin (suc n)

isTrue : Bool -> Set
isTrue true = True
isTrue false = False

isFalse : Bool -> Set
isFalse false = True
isFalse true = False

_<_ : Nat -> Nat -> Bool
_ < zero = false
zero < suc y = true
suc x < suc y = x < y

length : {A : Set} -> List A -> Nat
length [] = zero
length (x :: xs) = suc (length xs)

lookup : {A : Set} (xs : List A) (n : Nat) {_ : isTrue (n < length xs)} -> A
lookup [] p {}
lookup (x :: xs) zero = x
lookup (x :: xs) (suc n) {p} = lookup xs n {p}

nats : List Nat
nats = 1 :: 2 :: 3 :: []

result : Nat
result = lookup nats 2

infix 2 _==_
data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x

data _≤_ : Nat -> Nat -> Set where
  leq-zero : {n : Nat} -> zero ≤ n
  leq-suc : {m n : Nat} -> m ≤ n -> suc m ≤ suc n

leq-trans : {l m n : Nat} -> l ≤ m -> m ≤ n -> l ≤ n
leq-trans leq-zero _ = leq-zero
leq-trans (leq-suc x) (leq-suc y) = leq-suc (leq-trans x y)

data Vec (A : Set) : Nat -> Set where
  [] : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

_!_ : {n : Nat} {A : Set} -> Vec A n -> Fin n -> A
[] ! ()
(x :: xs) ! fzero = x
(x :: xs) ! fsuc i = xs ! i

natsV : Vec Nat _
natsV = 1 :: 2 :: 3 :: []

resultV : Nat
resultV = natsV ! fsuc fzero

_∘_ :
  {A : Set}
  {B : A -> Set}
  {C : (x : A) -> B x -> Set}
  (f : {x : A} (y : B x) -> C x y)
  (g : (x : A) -> B x)
  (x : A) ->
  C x (g x)
(f ∘ g) x = f (g x)

tabulate : {n : Nat} {A : Set} -> (Fin n -> A) -> Vec A n
tabulate {zero} f = []
tabulate {suc n} f = f fzero :: tabulate (f ∘ fsuc)

data Image_∋_ {A B : Set} (f : A -> B) : B -> Set where
  im : (x : A) -> Image f ∋ f x

inv : {A B : Set} (f : A -> B) (y : B) -> Image f ∋ y -> A
inv f .(f x) (im x) = x

min : Nat -> Nat -> Nat
min x y with x < y
min x y | true = x
min x y | false = y

filter : {A : Set} -> (A -> Bool) -> List A -> List A
filter p [] = []
filter p (x :: xs) with p x
... | true = x :: filter p xs
... | false = filter p xs

data _≠_ : Nat -> Nat -> Set where
  z≠s : {n : Nat} -> zero ≠ suc n
  s≠z : {n : Nat} -> suc n ≠ zero
  s≠s : {m n : Nat} -> m ≠ n -> suc m ≠ suc n

data Equal? (n m : Nat) : Set where
  eq : n == m -> Equal? n m
  neq : n ≠ m -> Equal? n m

equal? : (n m : Nat) -> Equal? n m
equal? zero zero = eq refl
equal? zero (suc m) = neq z≠s
equal? (suc n) zero = neq s≠z
equal? (suc n) (suc m) with equal? n m
equal? (suc n) (suc .n) | eq refl = eq refl
equal? (suc n) (suc m) | neq p = neq (s≠s p)

infix 2 _⊆_
data _⊆_ {A : Set} : List A -> List A -> Set where
  stop : [] ⊆ []
  drop : ∀ {xs y ys} -> xs ⊆ ys -> xs ⊆ y :: ys
  keep : ∀ {x xs ys} -> xs ⊆ ys -> x :: xs ⊆ x :: ys

lem-filter : {A : Set} (p : A -> Bool) (xs : List A) ->
  filter p xs ⊆ xs
lem-filter p [] = stop
lem-filter p (x :: xs) with p x
... | true = keep (lem-filter p xs)
... | false = drop (lem-filter p xs)

lem-plus-zero : (n : Nat) -> n + zero == n
lem-plus-zero zero = refl
lem-plus-zero (suc n) with n + zero | lem-plus-zero n
lem-plus-zero (suc n) | .n | refl = refl

Matrix : Set -> Nat -> Nat -> Set
Matrix A n m = Vec (Vec A n) m

vec : {n : Nat} {A : Set} -> A -> Vec A n
vec {zero} _ = []
vec {suc n} x = x :: vec {n} x

infix 90 _$_
_$_ : {n : Nat} {A B : Set} -> Vec (A -> B) n -> Vec A n -> Vec B n
[] $ [] = []
(f :: fs) $ (x :: xs) = f x :: fs $ xs

{-
1 2 3
4 5 6
-}
2x3 : Matrix Nat 2 3
2x3 =
  (1 :: 4 :: []) ::
  (2 :: 5 :: []) ::
  (3 :: 6 :: []) ::
  []

{-
1 4
2 5
3 6
-}
3x2 : Matrix Nat 3 2
3x2 =
  (1 :: 2 :: 3 :: []) ::
  (4 :: 5 :: 6 :: []) ::
  []

transpose : forall {A n m} -> Matrix A n m -> Matrix A m n
transpose = {!!}

lem-!-tab : ∀ {A n} (f : Fin n -> A) (i : Fin n) ->
  tabulate f ! i == f i
lem-!-tab = {!!}

lem-tab-! : ∀ {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs
lem-tab-! xs = {!!}



⊆-refl : {A : Set} {xs : List A} -> xs ⊆ xs
⊆-refl {xs = []} = stop
⊆-refl {xs = x :: xs} = keep ⊆-refl

⊆-trans : {A : Set} {xs ys zs : List A} ->
  xs ⊆ ys -> ys ⊆ zs -> xs ⊆ zs
⊆-trans stop q = q
⊆-trans p (drop q) = drop (⊆-trans p q)
⊆-trans (drop p) (keep q) = drop (⊆-trans p q)
⊆-trans (keep p) (keep q) = keep (⊆-trans p q)

data SubList {A : Set} : List A -> Set where
  [] : SubList []
  _::_ : ∀ x {xs} -> SubList xs -> SubList (x :: xs)
  skip : ∀ {x xs} -> SubList xs -> SubList (x :: xs)

forget : {A : Set} {xs : List A} -> SubList xs -> List A
forget [] = []
forget (x :: s) = x :: forget s
forget (skip s) = forget s

lem-forget : {A : Set} {xs : List A} (zs : SubList xs) -> forget zs ⊆ xs
lem-forget [] = stop
lem-forget (x :: zs) = keep (lem-forget zs)
lem-forget (skip zs) = drop (lem-forget zs)

filter' : {A : Set} -> (A -> Bool) -> (xs : List A) -> SubList xs
filter' p [] = []
filter' p (x :: xs) with p x
filter' p (x :: xs) | true = x :: filter' p xs
filter' p (x :: xs) | false = skip (filter' p xs)

complement : {A : Set} {xs : List A} -> SubList xs -> SubList xs
complement [] = []
complement (x :: zs) = skip (complement zs)
complement (skip {x = x} zs) = x :: complement zs

sublists : {A : Set} (xs : List A) -> List (SubList xs)
sublists [] = [] :: []
sublists (x :: xs) =
  map (\ys -> x :: ys) newSubLists ++
  map (\ys -> skip ys) newSubLists
  where newSubLists = sublists xs

data All {A : Set}(P : A -> Set) : List A -> Set where
  [] : All P []
  _::_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs)

data _∈_ {A : Set}(x : A) : List A -> Set where
  hd : forall {xs} -> x ∈ x :: xs
  tl : forall {y xs} -> x ∈ xs -> x ∈ y :: xs

index : forall {A}{x : A}{xs} -> x ∈ xs -> Nat
index hd = zero
index (tl p) = suc (index p)

data Lookup {A : Set}(xs : List A) : Nat -> Set where
  inside : (x : A)(p : x ∈ xs) -> Lookup xs (index p)
  outside : (m : Nat) -> Lookup xs (length xs + m)

lemma-All-∈ : forall {A x xs} {P : A -> Set} -> All P xs -> x ∈ xs -> P x
lemma-All-∈ [] ()
lemma-All-∈ (p :: ps) hd = p
lemma-All-∈ (p :: ps) (tl i) = lemma-All-∈ ps i

satisfies : {A : Set} -> (A -> Bool) -> A -> Set
satisfies p x = isTrue (p x)

data Inspect {A : Set}(x : A) : Set where
  it : (y : A) -> x == y -> Inspect x

inspect : {A : Set}(x : A) -> Inspect x
inspect x = it x refl

trueIsTrue : {x : Bool} -> x == true -> isTrue x
trueIsTrue refl = _
falseIsFalse : {x : Bool} -> x == false -> isFalse x
falseIsFalse refl = _


lem-filter-sound : {A : Set} (p : A -> Bool) (xs : List A) ->
  All (satisfies p) (filter p xs)
lem-filter-sound p [] = []
lem-filter-sound p (x :: xs) with inspect (p x)
lem-filter-sound p (x :: xs) | it y prf with p x | prf
--lem-filter-sound p (x :: xs) | it .true prf | true | refl = trueIsTrue prf :: lem-filter-sound p xs
lem-filter-sound p (x :: xs) | it .true prf | true | refl = {!!} :: lem-filter-sound p xs
lem-filter-sound p (x :: xs) | it .false prf | false | refl = lem-filter-sound p xs

not : Bool -> Bool
not true = false
not false = true

_◦_ : {A : Set}{B : A -> Set}{C : (x : A) -> B x -> Set} (f : {x : A}(y : B x) -> C x y)(g : (x : A) -> B x) (x : A) -> C x (g x)
(f ◦ g) x = f (g x)

data Find {A : Set}(p : A -> Bool) : List A -> Set where
  found : (xs : List A)(y : A) -> satisfies p y -> (ys : List A) -> Find p (xs ++ (y :: ys))
  not-found : forall {xs} -> All (satisfies (not ◦ p)) xs -> Find p xs

find : {A : Set}(p : A -> Bool)(xs : List A) -> Find p xs
find p [] = not-found []
find p (x :: xs) with inspect (p x)
... | it true prf = found [] x (trueIsTrue prf) xs
... | it false prf with find p xs
find p (x :: ._) | it false _ | found xs y py ys = found (x :: xs) y py ys
find p (x :: xs) | it false prf | not-found npxs = not-found ({!!} :: npxs)
--find p (x :: xs) | it false prf | not-found npxs = not-found ((falseIsFalse prf) :: npxs)

lem-filter-complete : {A : Set} (p : A -> Bool) (x : A) {xs : List A} ->
  x ∈ xs -> satisfies p x -> x ∈ filter p xs
lem-filter-complete p x {xs} el px = {!!}



postulate
  String : Set
{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE String String #-}


primitive
  primStringAppend   : String → String → String

infixl 50 _+++_
_+++_ : String → String → String
_+++_ = primStringAppend


Tag = String

mutual
  data Schema : Set where
    tag : Tag -> List Child -> Schema

  data Child : Set where
    text : Child
    elem : Nat -> Nat -> Schema -> Child

data BList (A : Set) : Nat -> Set where
  [] : ∀ {n} -> BList A n
  _::_ : ∀ {n} -> A -> BList A n -> BList A (suc n)

data Cons (A B : Set) : Set where
  _::_ : A -> B -> Cons A B

FList : Set -> Nat -> Nat -> Set
FList A zero m = BList A m
FList A (suc n) zero = False
FList A (suc n) (suc m) = Cons A (FList A n m)

mutual
  data XML : Schema -> Set where
    element : ∀ {kids} (t : Tag) -> All Element kids -> XML (tag t kids)

  Element : Child -> Set
  Element text = String
  Element (elem n m s) = FList (XML s) n m

mutual
  printXML : {s : Schema} -> XML s -> String
  printXML (element t x) =
    "<" +++ t +++ ">" +++
    (printChildren x) +++
    "</" +++ t +++ ">"

  printChildren : {kids : List Child} -> All Element kids -> String
  printChildren {[]} [] = ""
  printChildren {text :: kids} (x :: xs) = x +++ printChildren xs
  printChildren {elem n m s :: kids} (x :: xs) = {!!}

TutorialCompiled.agda

module TutorialCompiled where

data Unit : Set where
  unit : Unit
{-# COMPILED_DATA Unit () () #-}

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A -> Maybe A
{-# COMPILED_DATA Maybe Maybe Nothing Just #-}

postulate IO : Set -> Set
{-# BUILTIN IO IO #-}
{-# COMPILED_TYPE IO IO #-}

postulate
  String : Set
{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE String String #-}

postulate
  putStrLn : String -> IO Unit

{-# COMPILED putStrLn putStrLn #-}

data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A
{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _::_ #-}


main : IO Unit
main = putStrLn "Hello world!"

TutorialLambda.agda

module TutorialLambda where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

{-# BUILTIN NATURAL Nat  #-}

_+_ : Nat -> Nat -> Nat
0 + y = y
(suc x) + y = suc (x + y)

data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A
infixr 40 _::_

length : ∀ {A} -> List A -> Nat
length [] = zero
length (x :: xs) = suc (length xs)

data _∈_ {A : Set}(x : A) : List A -> Set where
  hd : forall {xs} -> x ∈ x :: xs
  tl : forall {y xs} -> x ∈ xs -> x ∈ y :: xs

index : forall {A}{x : A}{xs} -> x ∈ xs -> Nat
index hd = zero
index (tl p) = suc (index p)

data Lookup {A : Set}(xs : List A) : Nat -> Set where
  inside : (x : A)(p : x ∈ xs) -> Lookup xs (index p)
  outside : (m : Nat) -> Lookup xs (length xs + m)

_!_ : {A : Set}(xs : List A)(n : Nat) -> Lookup xs n
[] ! n = outside n
(x :: xs) ! zero = inside x hd
(x :: xs) ! suc n with xs ! n
(x :: xs) ! suc .(index p) | inside y p = inside y (tl p)
(x :: xs) ! suc .(length xs + n) | outside n = outside n


-- λ calculus

infixr 3 _=>_
data Type : Set where
  ı : Type
  _=>_ : Type -> Type -> Type

infix 2 _≠_
data _≠_ : Type -> Type -> Set where
  left-ı-right-fn : {σ τ : Type} -> ı ≠ σ => τ
  left-fn-right-ı : {σ τ : Type} -> σ => τ ≠ ı
  fn-domain-≠ : {σ₁ σ₂ τ : Type} -> σ₁ ≠ σ₂ -> (σ₁ => τ) ≠ (σ₂ => τ)
  fn-codomain-≠ : {σ τ₁ τ₂ : Type} -> τ₁ ≠ τ₂ -> (σ => τ₁) ≠ (σ => τ₂)
  fn-neither-≠ : {σ₁ σ₂ τ₁ τ₂ : Type} -> σ₁ ≠ σ₂ -> τ₁ ≠ τ₂ -> (σ₁ => τ₁) ≠ (σ₂ => τ₂)

data Equal? : Type -> Type -> Set where
  yes : ∀ {τ} -> Equal? τ τ
  no : ∀ {σ τ} -> σ ≠ τ -> Equal? σ τ

_=?=_ : (σ τ : Type) -> Equal? σ τ
ı =?= ı = yes
ı =?= (_ => _) = no left-ı-right-fn
(_ => _) =?= ı = no left-fn-right-ı
(σ₁ => τ₁) =?= (σ₂ => τ₂) with σ₁ =?= σ₂ | τ₁ =?= τ₂
(σ₁ => τ₁) =?= (.σ₁ => .τ₁) | yes | yes = yes
(σ₁ => τ₁) =?= (.σ₁ => τ₂) | yes | no p = no (fn-codomain-≠ p)
(σ₁ => τ₁) =?= (σ₂ => .τ₁) | no p | yes = no (fn-domain-≠ p)
(σ₁ => τ₁) =?= (σ₂ => τ₂) | no p₁ | no p₂ = no (fn-neither-≠ p₁ p₂)

infixl 8 _$_
data Raw : Set where
  var : Nat -> Raw
  _$_ : Raw -> Raw -> Raw
  lam : Type -> Raw -> Raw

Ctx = List Type

data Term (Γ : Ctx) : Type -> Set where
  var : ∀ {τ} -> τ ∈ Γ -> Term Γ τ
  _$_ : ∀ {σ τ} -> Term Γ (σ => τ) -> Term Γ σ -> Term Γ τ
  lam : ∀ σ {τ} -> Term (σ :: Γ) τ -> Term Γ (σ => τ)

erase : ∀ {Γ τ} -> Term Γ τ -> Raw
erase (var x) = var (index x)
erase (t $ u) = erase t $ erase u
erase (lam σ t) = lam σ (erase t)

data BadTerm (Γ : Ctx) : Set where
  var-outside : Raw -> BadTerm Γ
  app-bad-domain : BadTerm Γ -> Raw -> BadTerm Γ
  app-domain-ı : Raw -> BadTerm Γ
  app-bad-codomain : BadTerm Γ -> Raw -> BadTerm Γ
  mismatch-domain : Raw -> BadTerm Γ
  lam-expr : Raw -> BadTerm Γ

eraseBad : {Γ : Ctx} -> BadTerm Γ -> Raw
eraseBad (var-outside x) = x
eraseBad (app-bad-domain _ x) = x
eraseBad (app-domain-ı x) = x
eraseBad (app-bad-codomain _ x) = x
eraseBad (mismatch-domain x) = x
eraseBad (lam-expr x) = x

data Infer (Γ : Ctx) : Raw -> Set where
  ok : (τ : Type) (t : Term Γ τ) -> Infer Γ (erase t)
  bad : (b : BadTerm Γ) -> Infer Γ (eraseBad b)

infer : (Γ : Ctx) (e : Raw) -> Infer Γ e
infer Γ (var n) with Γ ! n
infer Γ (var .(length Γ + m)) | outside m = bad (var-outside (var (length Γ + m)))
infer Γ (var .(index x)) | inside σ x = ok σ (var x)
infer Γ (e1 $ e2) with infer Γ e1
infer Γ (.(eraseBad b) $ e2) | bad b = bad (app-bad-domain b ((eraseBad b) $ e2))
infer Γ (.(erase t) $ e2) | ok ı t = bad (app-domain-ı ((erase t) $ e2))
infer Γ (.(erase t) $ e2) | ok (σ => τ) t with infer Γ e2
infer Γ (.(erase t) $ .(eraseBad b)) | ok (σ => τ) t | bad b = bad (app-bad-codomain b ((erase t) $ (eraseBad b)))
infer Γ (.(erase t₁) $ .(erase t₂)) | ok (σ => τ) t₁ | ok σ′ t₂ with σ =?= σ′
infer Γ (.(erase t₁) $ .(erase t₂)) | ok (σ′ => τ) t₁ | ok .σ′ t₂ | yes = ok τ (t₁ $ t₂)
infer Γ (.(erase t₁) $ .(erase t₂)) | ok (σ => τ) t₁ | ok σ′ t₂ | no x = bad (mismatch-domain ((erase t₁) $ (erase t₂)) )
infer Γ (lam σ e) with infer (σ :: Γ) e
infer Γ (lam σ .(erase t)) | ok τ t = ok (σ => τ) (lam σ t)
infer Γ (lam σ .(eraseBad b)) | bad b = bad (lam-expr (lam σ (eraseBad b)))
{-
infer : (Γ : Ctx) (e : Raw) -> Infer Γ e
infer Γ (var n) with Γ ! n
infer Γ (var .(length Γ + n)) | outside n = bad
infer Γ (var .(index x)) | inside σ x = ok σ (var x)
infer Γ (e1 $ e2) with infer Γ e1
infer Γ (e1 $ e2) | bad = bad
infer Γ (.(erase t) $ e2) | ok ı t = bad
infer Γ (.(erase t) $ e2) | ok (σ => τ) t with infer Γ e2
infer Γ (.(erase t) $ e2) | ok (σ => τ) t | bad = bad
infer Γ (.(erase t₁) $ .(erase t₂)) | ok (σ => τ) t₁ | ok σ′ t₂ with σ =?= σ′
infer Γ (.(erase t₁) $ .(erase t₂)) | ok (σ′ => τ) t₁ | ok .σ′ t₂ | yes = ok τ (t₁ $ t₂)
infer Γ (.(erase t₁) $ .(erase t₂)) | ok (σ => τ) t₁ | ok σ′ t₂ | no = bad
infer Γ (lam σ e) with infer (σ :: Γ) e
infer Γ (lam σ .(erase t)) | ok τ t = ok (σ => τ) (lam σ t)
infer Γ (lam σ e) | bad = bad
-}

TutorialUniverses.agda

module TutorialUniverses where

data False : Set where
record True : Set where

data Bool : Set where
  true false : Bool

isTrue : Bool -> Set
isTrue true = True
isTrue false = False

infix 30 not_
infixr 25 _and_

not_ : Bool -> Bool
not true = false
not false = true

_and_ : Bool -> Bool -> Bool
true and b = b
false and _ = false

notNotId : (a : Bool) -> isTrue (not not a) -> isTrue a
notNotId true p = p
notNotId false ()

andIntro : (a b : Bool) -> isTrue a -> isTrue b -> isTrue (a and b)
andIntro true b p1 p2 = p2
andIntro false b () p2

{-
data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

{-# BUILTIN NATURAL Nat  #-}

nonZero : Nat -> Bool
nonZero zero = false
nonZero (suc n) = true

postulate _div_ : Nat -> (m : Nat) {p : isTrue (nonZero m)} -> Nat

three = 16 div 999
-}

data Functor : Set1 where
  |Id| : Functor
  |K| : Set -> Functor
  _|+|_ : Functor -> Functor -> Functor
  _|x|_ : Functor -> Functor -> Functor

data _⊕_ (A B : Set) : Set where
  inl : A -> A ⊕ B
  inr : B -> A ⊕ B

data _×_ (A B : Set) : Set where
  _,_ : A -> B -> A × B

infixr 50 _|+|_ _⊕_
infixr 60 _|x|_ _×_

[_] : Functor -> Set -> Set
[ |Id| ] X = X
[ (|K| A) ] X = A
[ (F |+| G) ] X = [ F ] X ⊕ [ G ] X
[ (F |x| G) ] X = [ F ] X × [ G ] X

map : (F : Functor) {X Y : Set} -> (X -> Y) -> [ F ] X -> [ F ] Y
map |Id| f x = f x
map (|K| x) f c = c
map (F |+| G) f (inl x) = inl (map F f x)
map (F |+| G) f (inr x) = inr (map G f x)
map (F |x| G) f (x , y) = map F f x , map G f y

data μ_ (F : Functor) : Set where
  <_> : [ F ] (μ F) -> μ F

mapFold : ∀ {X} F G -> ([ G ] X -> X) -> [ F ] (μ G) -> [ F ] X
mapFold |Id| G ϕ < x > = ϕ (mapFold G G ϕ x)
mapFold (|K| x) G ϕ c = c
mapFold (F₁ |+| F₂) G ϕ (inl x) = inl (mapFold F₁ G ϕ x)
mapFold (F₁ |+| F₂) G ϕ (inr y) = inr (mapFold F₂ G ϕ y)
mapFold (F₁ |x| F₂) G ϕ (x , y) = mapFold F₁ G ϕ x , mapFold F₂ G ϕ y

fold : {F : Functor} {A : Set} -> ([ F ] A -> A) -> μ F -> A
fold {F} ϕ < x > = ϕ (mapFold F F ϕ x)

NatF = |K| True |+| |Id|
NAT = μ NatF

Z : NAT
Z = < inl _ >

S : NAT -> NAT
S n = < inr n >

ListF = \A -> |K| True |+| |K| A |x| |Id|
LIST = \A -> μ (ListF A)

nil : {A : Set} -> LIST A
nil = < inl _ >

cons : {A : Set} -> A -> LIST A -> LIST A
cons x xs = < inr (x , xs) >

[_||_] : {A B C : Set} -> (A -> C) -> (B -> C) -> A ⊕ B -> C
[ f || g ] (inl x) = f x
[ f || g ] (inr y) = g y

uncurry : {A B C : Set} -> (A -> B -> C) -> A × B -> C
uncurry f (x , y) = f x y

const : {A B : Set} -> A -> B -> A
const x y = x

foldr : {A B : Set} -> (A -> B -> B) -> B -> LIST A -> B
foldr {A} {B} f z = fold [ const z || uncurry f ]

plus : NAT -> NAT -> NAT
plus n m = fold [ const m || S ] n


data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

{-# BUILTIN NATURAL Nat  #-}

infix 40 _+_
_+_ : Nat -> Nat -> Nat
zero + m = m
suc n + m = suc (n + m)

data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A
infixr 40 _::_

data Type : Set where
  bool : Type
  nat : Type
  list : Type -> Type
  pair : Type -> Type -> Type

El : Type -> Set
El bool = Bool
El nat = Nat
El (list t) = List (El t)
El (pair t1 t2) = El t1 × El t2

infix 30 _==_
_==_ : {a : Type} -> El a -> El a -> Bool

_==_ {nat} zero zero = true
_==_ {nat} zero (suc m) = false
_==_ {nat} (suc n) zero = false
_==_ {nat} (suc n) (suc m) = n == m

_==_ {bool} true x = x
_==_ {bool} false x = not x

_==_ {list a} [] [] = true
_==_ {list a} [] (x :: l2) = false
_==_ {list a} (x :: l1) [] = false
_==_ {list a} (x :: xs) (y :: ys) = x == y and xs == ys

_==_ {pair a b} (x1 , y1) (x2 , y2) = x1 == x2 and y1 == y2

example1 : isTrue (2 + 2 == 4)
example1 = _

example2 : isTrue (not (true :: false :: [] == true :: true :: []))
example2 = _

data Compare : Nat -> Nat -> Set where
  less : ∀ {n} k -> Compare n (n + suc k)
  more : ∀ {n} k -> Compare (n + suc k) n
  same : ∀ {n} -> Compare n n

compare : (n m : Nat) -> Compare n m
compare zero zero = same
compare zero (suc m) = less m
compare (suc n) zero = more n
compare (suc n) (suc m) with compare n m
compare (suc n) (suc .(n + suc k)) | less k = less k
compare (suc .(m + suc k)) (suc m) | more k = more k
compare (suc n) (suc .n) | same = same

difference : Nat -> Nat -> Nat
difference n m with compare n m
difference n .(n + suc k) | less k = zero
difference .(m + suc k) m | more k = k
difference n .n | same = zero