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

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

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

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

π2 : {U V : Set l} -> (U ×  V) -> V
π2 {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 l' : Level} (U : Set l)  ->  ((X : Set l) -> Emp  X) -> Emp  U
ε U t =  t U

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

lemma10 : {U V : Set l} -> {t :  U ×  V }  -> π1 ( ε ( U ×  V ) {!!} )  ≡ ε U {!!}
lemma10 = refl

-- lemma101 : {U V : Set l} -> {t :  U ×  V }  -> π2 ( ε {_} { U ×  V } t )  ≡ ε {_} {V} t
-- lemma101 = 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