module curry where

import swap

curry : (A B C:U) -> ((and A B) -> C) -> A -> B -> C
curry A B C f a b = f (a,b)

uncurry : (A B C:U) -> (A -> B -> C) -> (and A B) -> C
uncurry A B C g z = g z.1 z.2

eqCurry : (A B C : U) -> Id U ((and A B) -> C) (A -> B -> C)
eqCurry A B C =
 isEquivEq T V (curry A B C) (gradLemma T V (curry A B C) (uncurry A B C) (refl V) (refl T))
  where
   T:U
   T = (and A B) -> C
   V : U
   V = A -> B -> C

typFst : U
typFst = (X Y:U) -> (and X Y) -> X

typFst1 : U
typFst1 = (X Y:U) -> X -> Y -> X

eqTest : Id U typFst typFst1
eqTest = eqPi U  (\ X -> Pi U (\ Y -> (and X Y) -> X)) (\ X -> Pi U (\ Y -> X -> Y -> X)) rem
 where
  rem : (X:U) -> Id U (Pi U (\ Y -> (and X Y) -> X)) (Pi U (\ Y -> X -> Y -> X))
  rem X = eqPi U (\ Y -> (and X Y) -> X) (\ Y -> X -> Y -> X) rem1
    where
     rem1 : (Y:U) -> Id U ((and X Y) -> X) (X -> Y -> X)
     rem1 Y = eqCurry X Y X

eqTestInv : Id U typFst1 typFst
eqTestInv = inv U  ((X Y:U) -> (and X Y) -> X) ((X Y:U) -> X -> Y -> X) eqTest

test : N
test =
 transport typFst typFst1
  eqTest (\ X Y z -> z.1) N Bool zero true

test1 : N
test1 =
 transport typFst typFst1
  eqTest (\ X Y z -> z.1) N Bool (suc zero) false

test2 : N
test2 =
 transport typFst1 typFst
  eqTestInv (\ X Y a b -> a) N Bool (zero,true)

-- more test for the equality in U

eqTest2 : Id U typFst typFst
eqTest2 = comp U typFst typFst1 typFst eqTest eqTestInv

eqTest3 : Id U typFst typFst1
eqTest3 = comp U typFst typFst typFst1 eqTest2 eqTest

eqTest4 : Id U typFst typFst
eqTest4 = comp U typFst typFst1 typFst eqTest3 (inv U typFst typFst1 eqTest3)

test4 : N
test4 =
 transport typFst typFst
  eqTest2 (\ X Y z -> z.1) N Bool (suc zero,false)

test5 : N
test5 =
 transport typFst typFst1
  eqTest3 (\ X Y z -> z.1) N Bool (suc zero) false

test6 : N
test6 =
 transport typFst typFst
  eqTest4 (\ X Y z -> z.1) N Bool (suc zero,false)