module swap where

import gradLemma

-- the swap function defines an equality

swap : (A B :U) -> and A B -> and B A
swap A B = split
            pair a b -> pair b a

lemSwap : (A B:U) -> (z: and A B) -> Id (and A B) (swap B A (swap A B z)) z
lemSwap A B = split
               pair a b -> refl (and A B) (pair a b)

eqSwap : (A B :U) -> Id U (and A B) (and B A)
eqSwap A B = isEquivEq (and A B) (and B A) (swap A B) rem
 where
  rem : isEquiv (and A B) (and B A) (swap A B)
  rem = gradLemma (and A B) (and B A) (swap A B) (swap B A) (lemSwap B A) (lemSwap A B)

-- a simple test example

incr : and Bool N -> and Bool N
incr = split
     pair b n -> pair b (suc n)

incr' : and N Bool -> and N Bool
incr' = subst U (\ X -> X -> X) (and Bool N) (and N Bool) (eqSwap Bool N) incr

test6 : and N Bool
test6 = incr' (pair zero true)

test7 : and N Bool
test7 = incr' (pair (suc zero) true)

-- what happens if we compose eqSwap with itself?

eqSwap2 : (A B : U) -> Id U (and A B) (and A B)
eqSwap2 A B = comp U (and A B) (and B A) (and A B) (eqSwap A B) (eqSwap B A)

incr2 : and Bool N -> and Bool N
incr2 = subst U (\ X -> X -> X) (and Bool N) (and Bool N) (eqSwap2 Bool N) incr

test8 : and Bool N
test8 = incr2 (pair true zero)

test9 : and Bool N
test9 = incr2 (pair true (suc zero))

-- what happens if we compose eqSwap with its inverse?

eqSwap3 : (A B : U) -> Id U (and A B) (and A B)
eqSwap3 A B = comp U (and A B) (and B A) (and A B) (eqSwap A B) (inv U (and A B) (and B A) (eqSwap A B))

incr3 : and Bool N -> and Bool N
incr3 = subst U (\ X -> X -> X) (and Bool N) (and Bool N) (eqSwap2 Bool N) incr

test10 : and Bool N
test10 = incr3 (pair true zero)

test11 : and Bool N
test11 = incr3 (pair true (suc zero))


-- simple example with swap and product

eqPi : (A:U) -> (B0 B1 : A -> U) -> ((x:A)  -> Id U (B0 x) (B1 x)) -> Id U (Pi A B0) (Pi A B1)
eqPi A B0 B1 eB = cong (A->U) U (Pi A) B0 B1 rem
 where rem : Id (A -> U) B0 B1
       rem = funExt A (\ _ -> U) B0 B1 eB

eqSig : (A:U) -> (B0 B1 : A -> U) -> ((x:A)  -> Id U (B0 x) (B1 x)) -> Id U (Sigma A B0) (Sigma A B1)
eqSig A B0 B1 eB = cong (A->U) U (Sigma A) B0 B1 rem
 where rem : Id (A -> U) B0 B1
       rem = funExt A (\ _ -> U) B0 B1 eB

eqPiTest : Id U (Pi U (\ X -> X -> and X Bool)) (Pi U (\ X -> X -> and Bool X))
eqPiTest = eqPi U (\ X -> X -> and X Bool) (\ X -> X -> and Bool X) rem1
 where rem : (X:U) -> Id U (and X Bool) (and Bool X)
       rem X = eqSwap X Bool

       rem1 : (X:U) -> Id U (X -> and X Bool) (X -> and Bool X)
       rem1 X = eqPi X (\ _ -> and X Bool) (\ _ -> and Bool X) (\ _ -> rem X)

       
transPiTest : ((X:U) -> X -> and X Bool) -> (X:U) -> X -> and Bool X
transPiTest = transport  (Pi U (\ X -> X -> and X Bool)) (Pi U (\ X -> X -> and Bool X)) eqPiTest

test12 : and Bool N
test12 = transPiTest (\ X -> \ x -> pair x true) N zero

eqSigTest : Id U (Sigma U (\ X -> and X Bool)) (Sigma U (\ X -> and Bool X))
eqSigTest = eqSig U (\ X -> and X Bool) (\ X -> and Bool X) rem1
 where rem1 : (X:U) -> Id U (and X Bool) (and Bool X)
       rem1 X = eqSwap X Bool

transSigTest : (Sigma U (\ X -> and X Bool)) -> Sigma U (and Bool)
transSigTest = transport (Sigma U (\ X -> and X Bool)) (Sigma U (\ X -> and Bool X)) eqSigTest

test13 : U
test13 = fst U (and Bool) (transSigTest (pair Bool (pair false true)))

test14 : and Bool test13
test14 = snd U (and Bool) (transSigTest (pair Bool (pair false true)))

test15 : Bool
test15 = fst Bool (\ _ -> test13) test14

eqSig1Test : Id U (Sigma U (\ X -> and N Bool)) (Sigma U (\ X -> and Bool N))
eqSig1Test = eqSig U (\ X -> and N Bool) (\ X -> and Bool N) rem1
 where rem1 : (X:U) -> Id U (and N Bool) (and Bool N)
       rem1 X = eqSwap N Bool

transSig1Test : (and U (and N Bool)) -> and U (and Bool N)
transSig1Test = transport (and U (and N Bool)) (and U (and Bool N)) eqSig1Test

eqSig2Test : Id U (Sigma N (\ _ -> and N Bool)) (Sigma N (\ _ -> and Bool N))
eqSig2Test = eqSig N (\ _ -> and N Bool) (\ _ -> and Bool N) rem1
 where rem1 : N -> Id U (and N Bool) (and Bool N)
       rem1 n = eqSwap N Bool

transSig2Test : (Sigma N (\ X -> and N Bool)) -> Sigma N (\ _ -> and Bool N)
transSig2Test = transport (Sigma N (\ _ -> and N Bool)) (Sigma N (\ _ -> and Bool N)) eqSig2Test

test213 : N
test213 = fst N (\ _ -> and Bool N) (transSig2Test (pair zero (pair zero true)))

test214 : and Bool N
test214 = snd N (\ _ -> and Bool N) (transSig2Test (pair zero (pair zero true)))

test215 : Bool
test215 = fst Bool (\ _ -> N) test214

--- simple test

eqNN : Id U (and N N) (and N N)
eqNN = eqSwap N N

testNN : and N N
testNN = transport (and N N) (and N N) eqNN (pair zero (suc zero))

eqUU : Id U (U -> and U U) (U -> and U U)
eqUU = eqPi U (\ _ -> and U U) (\ _ -> and U U) (\ _ -> eqSwap U U)

testUU : U
testUU = fst U (\ _ -> U) (transport (U -> and U U) (U -> and U U) eqUU (\ X -> pair X X) Bool)