module swapDisc where

import lemId

-- defines the swap function over a discrete type and proves that this is an idempotent map
-- needed for Nicolai Kraus example

-- intermediate function

auxSwapD : (X:U) -> discrete X -> X -> X -> X -> X
auxSwapD X dX x0 x1 x = defCase (Id X x1 x) X x0 x (dX x1 x)

swapDisc : (X:U) -> discrete X -> X -> X -> X -> X
swapDisc X dX x0 x1 x = defCase (Id X x0 x) X x1 (auxSwapD X dX x0 x1 x) (dX x0 x)

idSwapDisc0 : (X:U) (dX: discrete X) -> (x0 x1 : X) -> (x:X) -> Id X x0 x -> 
     Id X (swapDisc X dX x0 x1 x) x1
idSwapDisc0 X dX x0 x1 x eqx0x =
 IdDefCasel (Id X x0 x) X x1 (auxSwapD X dX x0 x1 x) (dX x0 x) eqx0x

idSwapDiscn0 : (X:U) (dX: discrete X) -> (x0 x1 : X) -> (x:X) -> neg (Id X x0 x) -> 
              Id X (swapDisc X dX x0 x1 x) (auxSwapD X dX x0 x1 x)
idSwapDiscn0 X dX x0 x1 x neqx0x =
 IdDefCaser (Id X x0 x) X x1 (defCase (Id X x1 x) X x0 x (dX x1 x)) (dX x0 x) neqx0x

idAuxSwap1 :  (X:U) (dX: discrete X) -> (x0 x1 : X) -> (x:X) -> Id X x1 x -> 
              Id X (auxSwapD X dX x0 x1 x) x0
idAuxSwap1 X dX x0 x1 x eqx1x =
 IdDefCasel (Id X x1 x) X x0 x (dX x1 x) eqx1x

idAuxSwapn1 :  (X:U) (dX: discrete X) -> (x0 x1 : X) -> (x:X) -> neg (Id X x1 x) -> 
            Id X (auxSwapD X dX x0 x1 x) x
idAuxSwapn1 X dX x0 x1 x neqx1x = 
 IdDefCaser (Id X x1 x) X x0 x (dX x1 x) neqx1x

idSwapDisc1 : (X:U) (dX: discrete X) -> (x0 x1 : X) -> neg (Id X x0 x1) -> Id X (swapDisc X dX x0 x1 x1) x0
idSwapDisc1 X dX x0 x1 neqx0x1 = 
 comp X (swapDisc X dX x0 x1 x1) (defCase (Id X x0 x1) X x1 x0 (dX x0 x1)) x0 rem2 rem1
 where
  rem : Id X (defCase (Id X x1 x1) X x0 x1 (dX x1 x1)) x0
  rem = IdDefCasel (Id X x1 x1) X x0 x1 (dX x1 x1) (refl X x1)

  rem1 : Id X (defCase (Id X x0 x1) X x1 x0 (dX x0 x1)) x0
  rem1 = IdDefCaser (Id X x0 x1) X x1 x0 (dX x0 x1) neqx0x1

  rem2 : Id X (swapDisc X dX x0 x1 x1) (defCase (Id X x0 x1) X x1 x0 (dX x0 x1))
  rem2 = cong X X (\ y -> defCase (Id X x0 x1) X x1 y (dX x0 x1)) (defCase (Id X x1 x1) X x0 x1 (dX x1 x1)) x0 rem

-- can we show that swapDisc is idempotent??

idemSwapDisc : (X:U) (dX: discrete X) -> (x0 x1 : X) -> neg (Id X x0 x1) -> (x:X) -> 
               Id X (swapDisc X dX x0 x1 (swapDisc X dX x0 x1 x)) x 
idemSwapDisc X dX x0 x1 neqx0x1 x = orElim (Id X x0 x) (neg (Id X x0 x)) G rem9 rem11 (dX x0 x)
 where
   sD : X -> X
   sD = swapDisc X dX x0 x1 

   G : U
   G = Id X (sD (sD x)) x

   aD : X -> X
   aD = auxSwapD X dX x0 x1 

   rem : Id X x0 x -> Id X (sD x) x1
   rem = idSwapDisc0 X dX x0 x1 x  

   rem1 : neg (Id X x0 x) -> Id X (sD x) (aD x)
   rem1 = idSwapDiscn0 X dX x0 x1 x

   rem2 : Id X x1 x -> Id X (aD x) x0
   rem2 = idAuxSwap1 X dX x0 x1 x

   rem3 : neg (Id X x1 x) -> Id X (aD x) x
   rem3 = idAuxSwapn1 X dX x0 x1 x

   rem4 : Id X (aD x1) x0
   rem4 = idAuxSwap1 X dX x0 x1 x1 (refl X x1)

   rem5 : Id X (sD x1) (aD x1)
   rem5 = idSwapDiscn0 X dX x0 x1 x1 neqx0x1

   rem6 : Id X (sD x1) x0
   rem6 = comp X (sD x1) (aD x1) x0 rem5 rem4

   rem7 : Id X x0 x -> Id X (sD (sD x)) (sD x1)
   rem7 p = cong X X sD (sD x) x1 (rem p)

   rem8 : Id X x0 x -> Id X (sD (sD x)) x0
   rem8 p = comp X (sD (sD x)) (sD x1) x0 (rem7 p) rem6

   rem9 : Id X x0 x -> G
   rem9 p = comp X (sD (sD x)) x0 x (rem8 p) p

   rem10 : Id X (sD x0) x1
   rem10 = idSwapDisc0 X dX x0 x1 x0 (refl X x0)

   rem11 : neg (Id X x0 x) -> G
   rem11 neqx0x = orElim (Id X x1 x) (neg (Id X x1 x)) G rem14 rem15 (dX x1 x)
      where
        rem12 : Id X (sD x) (aD x)
        rem12 = rem1 neqx0x

        rem13 : Id X x1 x -> Id X (sD (aD x)) x1
        rem13 p = comp X (sD (aD x)) (sD x0) x1 (cong X X sD (aD x) x0 (rem2 p)) rem10

        rem14 : Id X x1 x -> G
        rem14 p = comp X (sD (sD x)) (sD (aD x)) x (cong X X sD (sD x) (aD x) rem12) (comp X (sD (aD x)) x1 x (rem13 p) p)

        rem15 : neg (Id X x1 x) -> G
        rem15 neqx1x = comp X (sD (sD x)) (sD x) x rem17 rem18
            where
             rem16 : Id X (aD x) x
             rem16 = rem3 neqx1x

             rem17 : Id X (sD (sD x)) (sD x)
             rem17 = comp X (sD (sD x)) (sD (aD x)) (sD x) (cong X X sD (sD x) (aD x) rem12) (cong X X sD (aD x) x rem16)

             rem18 : Id X (sD x) x
             rem18 = comp X (sD x) (aD x) x rem12 rem16