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 = {X : Set l} -> X -> X -> X

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

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

D : {U : Set l} -> U -> U -> Bool -> U
D {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}  -> Emp  -> Emp 
-- ε {l} {U} t =  t {l} {U}

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

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

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

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

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

-- lemma103 : {l : Level} {U V : Set l} -> (u : U) -> (t : Emp) -> ε (U -> V) 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 )

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)

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