open import Level
open import Relation.Binary.PropositionalEquality

module systemF {l : Level}  where

-- Bool

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

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

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

D : {X : Set} -> (U V : X) -> Bool -> X
D {X} u v bool = bool {X} u v

lemma-bool-t : {X : Set} -> {u v : X} -> D {X} u v T ≡ u
lemma-bool-t = refl

lemma-bool-f : {X : Set} -> {u v : X} -> D {X} u v F ≡ v
lemma-bool-f = refl

-- Product

_×_ : {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 : {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

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

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

-- Empty


-- Sum

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

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

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

δ : {l : Level} -> {U V : Set l} -> {X : Set l} -> (U -> X) -> (V -> X) -> (U + V) -> X
δ {l} {U} {V} {X} u v t = t {X} u v

lemma-sum-iota1 : {U V X R : Set l} -> {u : U} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι1 u) ≡ ux u
lemma-sum-iota1 = refl

lemma-sum-iota2 : {U V X R : Set l} -> {v : V} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι2 v) ≡ vx v
lemma-sum-iota2 = refl