ch1.ctt

module ch1 where

-- ex 1
-- Define composition of functions A -> B, functors
-- U -> U and composition operation for sigma types A x B -> B x C -> A x C. Also
-- write a generator of composition signature (A -> B) -> (B -> C) -> (A -> C).

fcomp (A B C : U) (f : A -> B) (g : B -> C) : A -> C = \(a : A) -> g (f a)

ffcomp (F G : U -> U) : U -> U = \(A : U) -> G (F A)

pcomp (A B C : U) (p1 : (_ : A) * B) (p2 : (_ : B) * C) : (_ : A) * C = (p1.1, p2.2)

-- ex 2
-- Define constant type and identity function.

const (A : U) (_ : A) : U = A 

id (A : U) (a : A) : const A a = a

-- ex 3
-- Show that any function of Pi-type equals
-- its left and right composition with identity function. Prove associativity of
-- composition.

Path (A : U) (a b : A) : U = PathP (<_> A) a b

refl (A : U) (a : A) : Path A a a = <_> a

runit (A B : U) (f : A -> B) : Path (A -> B) (fcomp A B B f (id B)) f = refl (A -> B) f

lunit (A B : U) (f : A -> B) : Path (A -> B) (fcomp A A B (id A) f) f = refl (A -> B) f

assoc (A B C D : U) (f : A -> B) (g : B -> C) (h : C -> D) : Path (A -> D) (fcomp A C D (fcomp A B C f g) h) (fcomp A B D f (fcomp B C D g h)) = refl (A -> D) (\(a: A) -> h (g (f a)))

-- ex 4
-- Define swap function

swap (A : U) (C : A -> A -> U) (f : (x y : A) -> C x y) : ((y x : A) -> C x y) = \(y x : A) -> f x y

-- ex 5
-- Define curry and uncury functions.

curry (A B C : U) (f : ((_ : A) * B) -> C) : A -> B -> C = \(a : A) -> \(b : B) -> f (a, b)

uncurry (A B C : U) (f : A -> B -> C) : ((_ : A) * B) -> C = \(p : (_ : A) * B) -> f p.1 p.2

-- ex 6
-- Define Sigma-type by using only Pi-type.

funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
       (p : (x : A) -> Path (B x) (f x) (g x)) :
       Path ((y : A) -> B y) f g = <i> \(a : A) -> (p a) @ i

Sigma (A : U) (B : A -> U) (a : A) : U = (C : A -> U) -> ((a1 : A) -> B a1 -> C a1) -> C a
deppair (A : U) (B : A -> U) (a : A) (b : B a) : Sigma A B a = \(C : A -> U) -> \(c : (a1 : A) -> B a1 -> C a1) -> c a b
pr1 (A : U) (B : A -> U) (a : A) (x : Sigma A B a) : A = x (\(_ : A) -> A) (\(a1 : A) -> \(_ : B a1) -> a1)
pr2 (A : U) (B : A -> U) (a : A) (x : Sigma A B a) : B a = x B (\(a1 : A) -> \(b : B a1) -> b)
Beta1 (A : U) (B : A -> U) (a : A) (b : B a) : Path A a (pr1 A B a (deppair A B a b)) = refl A a 
Beta2 (A : U) (B : A -> U) (a : A) (b : B a) : Path (B a) b (pr2 A B a (deppair A B a b)) = refl (B a) b
prf (A : U) (B : A -> U) (C : A -> U) (a : A) (c : (a1 : A) -> B a1 -> C a1) (x : Sigma A B a) : Path (C a) (x C c) (c a (x B (\(a1 : A) -> \(b : B a1) -> b))) = undefined --refl (C a) (x C c)
Eta2 (A : U) (B : A -> U) (a : A) (x : Sigma A B a) : Path (Sigma A B a) x (deppair A B a (pr2 A B a x)) = 
  funExt (A -> U) (\(C : A -> U) -> ((a1 : A) -> B a1 -> C a1) -> C a) x (deppair A B a (pr2 A B a x)) (\(C : A -> U) ->
    funExt ((a1 : A) -> B a1 -> C a1) (\(_ : (a1 : A) -> B a1 -> C a1) -> C a) (x C) (deppair A B a (pr2 A B a x) C) (\(c : (a1 : A) -> B a1 -> C a1) ->
      prf A B C a c x 
    )
  )

-- ex 7
-- Define the Fin-type by using only Sigma-type and recursion.
-- Define function that returns max element of Fin-set.

data nat = zero
         | suc (n : nat)

one   : nat = suc zero
two   : nat = suc one
three : nat = suc two
four  : nat = suc three
five  : nat = suc four

pred: nat -> nat = split
  zero -> zero
  suc n -> n

-- data Vect : Nat -> Type -> Type where
--   Nil  : Vect Z a
--   (::) : a -> Vect k a -> Vect (S k) a

data vector (A : U) (n : nat)
   = vzero
   | vsuc (_ : A) (_ : vector A (pred n))

vz (A : U) : vector A zero = vzero
vs (A : U) (x : A) (n : nat) (xs : vector A n) : vector A (suc n) = vsuc x xs

opaque vector

vec : vector nat three = vs nat five two (vs nat four one (vs nat three zero (vz nat)))

--data Fin : Nat -> Type where
--   FZ : Fin (S k)
--   FS : Fin k -> Fin (S k)

data Fin (n : nat) = fzero | fsuc (_ : Fin (pred n))

fz (n : nat) : Fin (suc n) = fzero
fs (n : nat) (x : Fin n) : Fin (suc n) = fsuc x

opaque Fin

fin11 : Fin one   = fz zero
fin21 : Fin two   = fz one
fin22 : Fin two   = fs one fin11
fin31 : Fin three = fz two
fin32 : Fin three = fs two fin21
fin33 : Fin three = fs two fin22

max : (n : nat) -> Fin (suc n) = split
  zero -> fz zero
  suc k -> fs (suc k) (max k)

add__ (m : nat) : nat -> nat = split
  zero  -> m
  suc n -> suc (add__ m n)

Fin_ (n : nat) : U = (m k : nat) * Path nat (add__ m (suc k)) n

fin11_ : Fin_ one   = (zero, zero, refl nat one)
fin21_ : Fin_ two   = (zero, one, refl nat two)
fin22_ : Fin_ two   = (one, zero, refl nat two)
fin31_ : Fin_ three = (zero, two, refl nat three)
fin32_ : Fin_ three = (one, one, refl nat three)
fin33_ : Fin_ three = (two, zero, refl nat three)

max_ (n : nat) : Fin_ (suc n) = (n, zero, refl nat (suc n))

data Unit = unit

-- ex 8
-- Define W-type by using only Sigma-type.

W (A : U) (B : A -> U) : U = (x : A) * (B x -> W A B)
Wrec (A : U) (B : A -> U) (P : U) (alg: (a : A) -> (B a -> W A B) -> (B a -> P) -> P)
   : W A B -> P = \(w : W A B) -> alg w.1 w.2 (\(b : B w.1) -> Wrec A B P alg (w.2 b))
Wind (A : U) (B : A -> U) (P : W A B -> U) (alg: (a : A) (f : B a -> W A B) -> ((b : B a) -> P (f b)) -> P (a, f))
   : (w: W A B) -> P w = \(w : W A B) -> alg w.1 w.2 (\(b : B w.1) -> Wind A B P alg (w.2 b))

-- ex 9
-- Define Nat-type as W-type. Also define a Nat algebra:
-- multiplication, power, factorial by using recNat.

-- N^w :≡ W(b:2) rec_2(U, 0, 1, b)

data Void = void

opaque Void

absurd : (A : U) -> Void -> A = undefined

data bool = false | true

Bnat : bool -> U = split
  false -> Void
  true  -> Unit

natw : U = W bool Bnat

recnat_ (P : U) (alg: (a : bool) -> (Bnat a -> natw) -> (Bnat a -> P) -> P)
  : natw -> P = Wrec bool Bnat P alg

recnat (A : U) (a : A) (f : nat -> A -> A) : nat -> A = split
  zero  -> a
  suc n -> f n (recnat A a f n)

recnat__ (A : U) (a : A) (f : natw -> A -> A) 
  : natw -> A = let alg : (b : bool) -> (Bnat b -> natw) -> (Bnat b -> A) -> A = split
                      false -> \(_ : Void -> natw) -> \(_ : Void -> A) -> a
                      true  -> \(g : Unit -> natw) -> \(h : Unit -> A) -> f (g unit) (h unit)
                in recnat_ A alg

zero_ : natw = (false, absurd natw)
suc_ (n : natw) : natw = (true, \(_ : Unit) -> n)

one_ : natw = suc_ zero_
two_ : natw = suc_ one_
three_ : natw = suc_ two_
four_ : natw = suc_ three_
five_ : natw = suc_ four_

-- 0 + m = m
-- Sn + m = S(n+m)
add (n : natw) : natw -> natw = recnat__ natw n (\(_ : natw) -> \(s : natw) -> suc_ s)

add_ : natw -> natw -> natw = recnat__ (natw -> natw) (id natw) (\(n : natw) -> \(addn : natw -> natw) -> \(m : natw) -> suc_ (addn m))

-- 0 * m = 0
-- Sn * m = n*m + m
mult (n : natw) : natw -> natw = recnat__ natw zero_ (\(_ : natw) -> \(p : natw) -> add p n)

-- n^0 = 1
-- n^Sm = n^m * n
pow (n : natw) : natw -> natw = recnat__ natw one_ (\(_ : natw) -> \(p : natw) -> mult p n)

-- ex 10
-- Define List-type as W-type.

data list (A : U) = nil 
                  | cons (a : A) (as : list A)

-- List(A) :≡ W(x:1+A) rec_{1 + A}(U, 0, λa.1, x)

data orUnit (A : U) = orUnitL | orUnitR (a : A)

Blist (A : U) : orUnit A -> U = split
  orUnitL   -> Void
  orUnitR _ -> Unit

listw (A : U) : U = W (orUnit A) (Blist A)

reclist (A : U) (P : U) (alg: (a : orUnit A) -> (Blist A a -> listw A) -> (Blist A a -> P) -> P)
   : listw A -> P = Wrec (orUnit A) (Blist A) P alg

reclist_ (A : U) (P : U) (p : P) (f : A -> listw A -> P -> P) 
   : listw A -> P = let alg : (a : orUnit A) -> (Blist A a -> listw A) -> (Blist A a -> P) -> P = split
                          orUnitL    -> \(_ : Void -> listw A) -> \(_ : Void -> P) -> p
                          orUnitR a  -> \(g : Unit -> listw A) -> \(h : Unit -> P) -> f a (g unit) (h unit)
                    in reclist A P alg

nil_ (A : U) : listw A = (orUnitL, absurd (listw A))
cons_ (A : U) (a : A) (as : listw A) : listw A = (orUnitR a, \(_ : Unit) -> as)

l : listw nat = cons_ nat one (cons_ nat two (cons_ nat three (nil_ nat)))

length (A : U) (l : listw A) : nat = reclist_ A nat zero (\(a : A) -> \(as : listw A) -> \(as_len : nat) -> suc as_len) l

-- ex 11
-- Define Ackermann function by using only recNat.

--ack(0, n) ≡ succ(n),
--ack(succ(m), 0) ≡ ack(m, 1),
--ack(succ(m), succ(n)) ≡ ack(m, ack(succ(m), n))              

ack : natw -> natw -> natw = recnat__ (natw -> natw) (\(m : natw) -> suc_ m) (\(n : natw) -> \(ackn : natw -> natw) -> \(m : natw) ->
  recnat__ natw (ackn one_) (\(m1 : natw) -> \(ackSnm1 : natw) -> ackn ackSnm1) m  )
--                                                                ackSnSm1