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 (pair a b)

uncurry : (A B C:U) -> (A -> B -> C) -> (and A B) -> C
uncurry A B C g = split
                    pair a b -> g a b

secCurry : (A B C :U) (f : (and A B) -> C) 
            -> Id ((and A B) -> C) (uncurry A B C (curry A B C f)) f
secCurry A B C f = funExt (and A B) (\ _ -> C) (uncurry A B C (curry A B C f)) f rem
 where 
  rem : (z:and A B) -> Id C (uncurry A B C (curry A B C f) z) (f z)
  rem = split
         pair a b -> refl C (f (pair a b))

retCurry : (A B C :U) (g : A -> B -> C)
            -> Id (A -> B -> C) (curry A B C (uncurry A B C g)) g
retCurry A B C g = funExt A (\ _ -> B -> C) (curry A B C (uncurry A B C g)) g rem
 where 
  rem : (a:A) -> Id (B -> C) (curry A B C (uncurry A B C g) a) (g a)
  rem a = funExt B (\ _ -> C) (curry A B C (uncurry A B C g) a) (g a) rem1
     where
       rem1 : (b:B) -> Id C (curry A B C (uncurry A B C g) a b) (g a b)
       rem1 b = refl C (g a b)


eqCurry : (A B C : U) -> Id U ((and A B) -> C) (A -> B -> C)
eqCurry A B C = isEquivEq ((and A B) -> C) (A -> B -> C) (curry A B C) rem
  where
   rem : isEquiv ((and A B) -> C) (A -> B -> C) (curry A B C) 
   rem =  gradLemma ((and A B) -> C) (A -> B -> C) 
                 (curry A B C) (uncurry A B C) (retCurry A B C) (secCurry 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 -> (fst X (\ _ -> Y))) N Bool zero true
      
test1 : N
test1 =
 transport typFst typFst1
  eqTest (\ X Y -> (fst X (\ _ -> Y))) N Bool (suc zero) false

test2 : N
test2 = 
 transport typFst1 typFst
  eqTestInv (\ X Y a b -> a) N Bool (pair 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 -> (fst X (\ _ -> Y))) N Bool (pair (suc zero) false)

test5 : N
test5 =
 transport typFst typFst1
  eqTest3 (\ X Y -> (fst X (\ _ -> Y))) N Bool (suc zero) false

test6 : N
test6 =
 transport typFst typFst
  eqTest4 (\ X Y -> (fst X (\ _ -> Y))) N Bool (pair (suc zero) false)