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 = {!!}