open import Level
open import Relation.Binary.PropositionalEquality

module systemF 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 : Set l} -> {V : Set l} -> U -> V -> (U × V)
<_,_> {l} {U} {V} u v = \{X : Set l} -> \(x : U -> V -> X) -> x u v

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

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

lemma-product : {l : Level} {U V : Set l} -> U -> V -> U × V
lemma-product u v = < u , v >

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

lemma-product-pi2 : {l : Level} {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 :  {l : Level} {U V : Set l} -> U -> (U + V)
ι1  {l} {U} {V} u =  \{X : Set l} -> \(x : U -> X) -> \(y : V -> X) -> x u

ι2 : {l : Level} {U V : Set l} -> V -> (U + V)
ι2  {l} {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 : {l : Level} {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 : {l : Level} {U V X R : Set l} -> {v : V} -> {ux : (U -> X)} -> {vx : (V -> X)} -> δ ux vx (ι2 v) ≡ vx v
lemma-sum-iota2 = refl


-- Existential

data V {l} (X : Set l) : Set l
  where
    v : X -> V X

Σ_,_ : {l : Level} (X : Set l) -> V X -> Set (suc l)
Σ_,_ {l} U u = {Y : Set l} -> ({X : Set l} -> (V X) -> Y) -> Y

⟨_,_⟩ : {l : Level} (U : Set l) -> (u : V U) -> Σ U , u
⟨_,_⟩ {l} U u = \{Y : Set l} -> \(x : {X : Set l} -> (V X) -> Y) -> x {U} u

∇_,_,_ :  {l : Level} {W : Set l} -> (X : Set l) -> { u : V X } -> X -> W -> Σ X , u  -> W
∇_,_,_ {l} {W} X {u} x w t = t {W} (\{X : Set l} -> \(x : V X) -> w)

{-
  lemma-nabla on proofs and types
  (∇ X , x , w ) ⟨ U , u ⟩ ≡ w
  w[U/X][u/x^[U/X]]
-}

lemma-nabla : {l : Level} {X W : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {l} {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w
lemma-nabla = refl


-- Int

Int : {l : Level} -> {X : Set l} -> Set l
Int {l} {X} = X -> (X -> X) -> X

O : {l : Level} -> {X : Set l} -> Int
O {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)

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

lemma-it-o : {l : Level} {U : Set l} -> {u : U} -> {f : U -> U} -> It u f O ≡ u
lemma-it-o = refl

lemma-it-s-o : {l : Level} {U : Set l} -> {u : U} -> {f : U -> U} -> {t : Int} -> It u f (S t) ≡ f (It u f t)
lemma-it-s-o = refl

g : {l : Level} -> {U : Set l} -> {f : U -> Int {l} {U} -> U} -> (U × Int) -> (U × Int)
g {l} {U} {f} = \x -> < (f (π1 x) (π2 x)) , S (π2 x) >

-- cannot prove general Int
-- lemma-it-n : {l : Level} {U : Set l} {u : U} {n : Int} {f : U -> Int -> U} -> g {l} {U} {f} < u , n > ≡ < f u n , S n >
-- lemma-it-n = refl

R : {l : Level} -> {U : Set l} -> U -> (U -> Int -> U) -> Int -> U
R {l} {U} u f t = π1 (It {suc l} {U × Int} < u , O > (g {_} {_} {f}) t)

lemma-R-O : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} -> R u f O ≡ u
lemma-R-O = refl

lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) (n < u , O > (g {l} {U} {f}) (\u n ->  π2 < u , n > ))
lemma-R-n = refl

-- Proofs And Types Style lemma-R-n
-- lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) n
-- n in (S n) and (R u f n) has (U × Int), but last n has Int.
-- regenerate same (n : Int) by used g, <_,_>
-- NOTE : Proofs And Types say "equation for recursion is satisfied by values only"


-- List

List : {l : Level} -> (U : Set l) -> Set (suc l)
List {l} U = {X : Set l} -> X -> (U -> X -> X) -> X

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

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

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

lemma-list-it-nil : {l : Level} {U W : Set l} {w : W} {f : U -> W -> W} -> ListIt w f nil ≡ w
lemma-list-it-nil = refl

lemma-list-it-cons : {l : Level} {U W : Set l} {u : U} {w : W} {f : U -> W -> W} {t : List U} -> ListIt w f (cons u t) ≡ f u (ListIt w f t)
lemma-list-it-cons = refl