open import Level
open import Relation.Binary.PropositionalEquality

module system-f  where

Bool : {l : Level} (X : Set l) -> Set l
Bool = \{l : Level} -> \(X : Set l) -> X -> X -> X

T : {l : Level} (X : Set l) -> Bool X
T X = \(x y : X) -> x

F : {l : Level} (X : Set l) -> Bool X
F X = \(x y : X) -> y

D : {l : Level} -> {U : Set l} -> U -> U -> Bool U -> U
D u v t = t u v

lemma04 : {l : Level} { U : Set l} {u v : U} -> D {_} {U} u v (T U ) ≡  u
lemma04 = refl

lemma05 : {l : Level} { U : Set l} {u v : U} -> D {_} {U} u v (F U ) ≡  v
lemma05 = refl

_×_ : {l : Level} -> Set l -> Set l ->  Set (suc l)
_×_ {l} U V =  {X : Set l} -> (U -> V -> X)  -> X 

<_,_> : {l : Level} {U V : Set l} -> U -> V -> (U ×  V) 
<_,_> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v

π1 : {l : Level} {U V : Set l} -> (U ×  V) -> U
π1 {l} {U} {V}  t = t {U} (\(x : U) -> \(y : V) -> x)

π2 : {l : Level} {U V : Set l} -> (U ×  V) -> V
π2 {l} {U} {V}  t = t {V} (\(x : U) -> \(y : V) -> y)

lemma06 : {l : Level} {U V : Set l } -> {u : U } -> {v : V} -> π1 ( < u , v > ) ≡  u
lemma06 = refl

lemma07 : {l : Level} {U V : Set l } -> {u : U } -> {v : V} -> π2 ( < u , v > ) ≡  v
lemma07 = refl

hoge : {l : Level} {U V : Set l} -> U -> V  -> (U ×  V)
hoge u v = < u , v >

-- lemma08 :  (t : U ×  V)  -> < π1 t  , π2 t > ≡ t
-- lemma08 t = {!!}

-- Emp definision is still wrong...

Emp  :  {l : Level} {X : Set l} ->  Set l
Emp {l} = \{X : Set l} -> X

-- ε :  {l : Level} (U : Set l)  {l' : Level} {U' : Set l'}  -> Emp -> Emp 
-- ε {l} U t =  t 

-- lemma09 : {l : Level} {U : Set l} {l' : Level} {U' : Set l} -> (t : Emp {l} {U} ) -> ε U (ε Emp t) ≡ ε U t
-- lemma09 t = refl

-- lemma10 :  {l : Level} {U V X : Set l} ->  (t : Emp {_} {U ×  V}) -> U × V
-- lemma10  {l} {U} {V} t = ε (U ×  V) t

-- lemma10' : {l : Level} {U V X : Set l} ->  (t : Emp {_} {U ×  V}) -> Emp
-- lemma10' {l} {U} {V} {X} t = ε (U ×  V) t 

-- lemma100 : {l : Level} {U V X : Set l} ->  (t : Emp {_} {U}) -> Emp
-- lemma100 {l} {U} {V} t = ε U t

-- lemma101 : {l k : Level} {U V : Set l} ->  (t : Emp {_} {U × V}) -> π1 (ε (U ×  V) t) ≡ ε U t
-- lemma101 t = refl

-- lemma102 : {l k : Level} {U V : Set l} ->  (t : Emp {_} {U × V}) -> π2 (ε (U ×  V) t) ≡ ε V t
-- lemma102 t = refl

-- lemma103 : {l : Level} {U V : Set l} -> (u : U) -> (t : Emp {l} {_} ) -> (ε (U -> V) t) u ≡ ε V t
-- lemma103 u t = refl

_+_  : {l : Level} -> Set l -> Set l -> Set (suc l)
_+_ {l} U V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X

ι1 : {l : Level } {U V : Set l} ->  U ->  U + V
ι1 {l} {U} {V} u = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> x u

ι2 : {l : Level } {U V : Set l} ->  V ->  U + V
ι2 {l} {U} {V} v = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> y v

δ : {l : Level} { U V R S : Set l } -> (R -> U) -> (S -> U) -> ( R + S ) -> U
δ {l} {U} {V} {R} {S} u v t = t {U} (\(x : R) -> u x) ( \(y : S) -> v y)

lemma11 : {l : Level} { U V R S : Set _ } -> (u : R -> U ) (v : S -> U ) -> (r : R) -> δ {l} {U} {V} {R} {S} u v ( ι1 r )  ≡ u r
lemma11 u v r =  refl

lemma12 : {l : Level} { U V R S : Set _ } -> (u : R -> U ) (v : S -> U ) -> (s : S) -> δ {l} {U} {V} {R} {S} u v ( ι2 s )  ≡ v s
lemma12 u v s =  refl


_××_ : {l : Level} -> Set (suc l) -> Set l ->  Set (suc l)
_××_ {l} U V =  {X : Set l} -> (U -> V -> X)  -> X 

<<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} -> U -> V -> (U  ××   V) 
<<_,_>> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v


Int : {l : Level } ( X : Set l ) -> Set l
Int {l} X = X -> ( X -> X ) -> X

Zero : {l : Level } -> { X : Set l } -> Int X
Zero {l} {X} = \(x : X ) -> \(y : X -> X ) -> x

S : {l : Level } -> { X : Set l } -> Int X -> Int X
S {l} {X} t = \(x : X) -> \(y : X -> X ) -> y ( t x y )

n0 : {l : Level} {X : Set l} -> Int X
n0 = Zero 

n1 : {l : Level } -> { X : Set l } -> Int X
n1 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y x

n2 : {l : Level } -> { X : Set l } -> Int X
n2 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y x)

n3 : {l : Level } -> { X : Set l } -> Int X
n3 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y x))

n4 : {l : Level } -> { X : Set l } -> Int X
n4 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y (y x)))

lemma13 : {l : Level } -> { X : Set l } -> S (S (Zero {_} {X}))  ≡ n2 
lemma13 = refl

It : {l : Level} {U : Set l} -> U -> ( U -> U ) -> Int U -> U
It {l} {U} u f t = t u f

R : {l : Level} { U X : Set l}   -> U -> ( U -> Int X ->  U ) -> Int _ -> U 
R {l} {U} {X} u v t =  π1 ( It {suc l} {U ×  Int X} (< u , Zero >) (λ (x : U × Int X) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 

add : {l : Level} {X : Set l} -> Int X -> Int X -> Int X
add x y = \z t -> x (y z t) t

mul : {l : Level } {X : Set l} -> Int X -> Int (Int X) -> Int X
mul {l} {X} x y = It Zero (add x) y

fact : {l : Level} {X : Set l} -> Int _ -> Int X
fact  {l} {X} n = R (S Zero) (λ z -> λ w -> mul z (S w) ) n

lemma13' : {l : Level} {X : Set l} -> fact {l} {X} n4 ≡ mul n4 ( mul n2 n3)
lemma13' = refl

-- lemma14 : {l : Level} {X : Set l} -> (x y : Int X) -> mul x y  ≡ mul y x
-- lemma14 x y = It {!!} {!!} {!!}

lemma15 : {l : Level} {X : Set l} (x y : Int X) -> mul {l} {X} n2 n3  ≡ mul {l} {X} n3 n2
lemma15 x y = refl

lemma16 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int X ->  U ) -> R u v Zero ≡ u
lemma16 u v = refl

-- lemma17 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int ->  U ) -> (t : Int ) -> R u v (S t) ≡ v ( R u v t ) t
-- lemma17 u v t = refl

-- postulate lemma17 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int ->  U ) -> (t : Int ) -> R u v (S t) ≡ v ( R u v t ) t

List : {l : Level} (U X : Set l) -> Set l
List {l} = \( U X : Set l)  -> X -> ( U -> X ->  X ) -> X 

Nil : {l : Level} {U : Set l} {X : Set l} -> List U X
Nil {l} {U} {X} = \(x : X) -> \(y : U -> X -> X) -> x

Cons : {l : Level} {U : Set l} {X : Set l} -> U -> List U X -> List U X
Cons {l} {U} {X} u t = \(x : X) -> \(y : U -> X -> X) -> y u (t x y )

l0 : {l : Level} {X X' : Set l} -> List (Int X) (X')
l0 = Nil

l1 : {l : Level} {X X' : Set l} -> List (Int X) (X')
l1 = Cons n1 Nil

l2 : {l : Level} {X X' : Set l} -> List (Int X) (X')
l2 = Cons n2 l1

l3 : {l : Level} {X X' : Set l} -> List (Int X) (X')
l3 = Cons n3 l2

ListIt : {l : Level} {U W X : Set l} -> W -> ( U -> W -> W ) -> List U W -> W
ListIt w f t = t w f

Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List U (Bool X) -> Bool _
Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool _} {X} (T X) (\u w -> (F X)) list

Append : {l : Level} {U : Set l} {X : Set l} -> List U _ -> List U X -> List U _
Append x y = \s t -> x (y s t) t

lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {_} {Int U} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
lemma18 = refl

Reverse : {l : Level} {U : Set l} {X : Set l} -> List U _ -> List U X
Reverse {l} {U} {X} x = ListIt {_} {U} {List U _} {X} Nil ( \u w -> Append w (Cons u Nil) ) x

lemma19 :{l : Level} {U : Set l} {X : Set l} -> Reverse {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil))
lemma19 = refl

Tree : {l : Level} -> Set l -> Set l -> Set l
Tree {l} = \( U X : Set l)  -> X -> ( (U -> X) ->  X ) -> X

NilTree : {l : Level} (U : Set l) (X : Set l) -> Tree U X
NilTree U X = \(x : X) -> \(y : (U -> X) -> X) -> x

Collect : {l : Level} (U : Set l) (X : Set l) -> (U -> X -> ((U -> X) -> X) -> X ) -> Tree U X
Collect U X f = \(x : X) -> \(y : (U -> X) -> X) -> y (\(z : U) -> f z x y )

TreeIt : {l : Level} {U W X : Set l} -> W -> ( (U -> W) -> W ) -> Tree U W -> W
TreeIt w h t = t w h