open import Level
open import Relation.Binary.PropositionalEquality

module system-f {l : Level} where

postulate A : Set
postulate B : Set

data _∨_  (A B : Set) : Set where
  or1 : A -> A ∨ B
  or2 : B -> A ∨ B

lemma01 : A -> A ∨ B
lemma01 a = or1 a

lemma02 : B -> A ∨ B
lemma02 b = or2 b

lemma03 : {C : Set} -> (A ∨ B) -> (A -> C) -> (B -> C) -> C
lemma03 (or1 a) ac bc = ac a
lemma03 (or2 b) ac bc = bc b

postulate U : Set l
postulate V : Set l


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

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

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

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

lemma04 : {u v : U} -> D u v T ≡  u
lemma04 = refl

lemma05 : {u v : U} -> D u v F ≡  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 : {U V : Set l } -> {u : U } -> {v : V} -> π1 ( < u , v > ) ≡  u
lemma06 = refl

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

hoge : {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

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

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

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

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

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

lemma12 : { U V R S : Set l } -> (u : R -> U ) (v : S -> U ) -> (s : S) -> δ  {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 } -> X -> ( X -> X ) -> X

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

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

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

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

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

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

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

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


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

sum : {l : Level} {X : Set l} -> Int -> Int {l} {X} -> Int
sum x y = It y ( λ z -> S z ) x

mul : {l : Level } {X : Set l} -> Int {l} {_} -> Int  -> Int {l} {X}
mul  x y = It Zero ( λ (z : Int) -> sum y z ) x

copyInt : {l : Level } {X : Set l} -> Int {l} {_} -> Int {l} {X}
copyInt  x = It Zero ( λ (z : Int) -> S z ) x

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

-- lemma13' : fact n3 ≡ mul n1 ( mul n2 n3)
-- lemma13' = refl

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

lemma15 : {l : Level} {X : Set l} (x y : Int {l} {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 {l} {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}  -> X -> ( U -> X ->  X ) -> X

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

Cons : {l : Level} {U : Set l} {X : Set l} -> U -> List {l} {U} {X} -> List {l} {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 {l} {Int {l} {X}} {X'}
l0 = Nil

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

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

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

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

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

lemma18 : Append l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
lemma18 = refl

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

NilTree : {l : Level} {U : Set l} {X : Set l} -> Tree {l} {U} {X}
NilTree {l} {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 {l} {U} {X}
Collect {l} {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 {l} {U} {W} -> W
TreeIt {l} {U} {W} {X} w h t = t w h