module swap where

import gradLemma

-- the swap function defines an equality

and : U -> U -> U
and A B = (_ : A) * B

swap : (A B :U) -> and A B -> and B A
swap A B z = (z.2,z.1)

lemSwap : (A B:U) -> (z: and A B) -> Id (and A B) (swap B A (swap A B z)) z
lemSwap A B z = refl (and A B) z

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 z = (z.1,suc z.2)

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

test1 : and N Bool
test1 = incr' (zero,true)

test2 : and N Bool
test2 = incr' (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

test3 : and Bool N
test3 = incr2 (true,zero)

test4 : and Bool N
test4 = incr2 (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

test5 : and Bool N
test5 = incr3 (true,zero)

test6 : and Bool N
test6 = incr3 (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 = mapOnPath (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 = mapOnPath (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 -> (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

test7 : U
test7 = (transSigTest (Bool,(false,true))).1

test8 : and Bool test7
test8 = (transSigTest (Bool,(false,true))).2

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

test9 : N
test9 = (transSig2Test (zero,(zero,true))).1

test10 : and Bool N
test10 =  (transSig2Test (zero,(zero,true))).2

--- 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 (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 = (transport (U -> and U U) (U -> and U U) eqUU (\ X -> (X,X)) Bool).1