module swapDisc_old where

import lemId
import involutive
import contr
import elimEquiv


-- definition by case on a decidable equality
-- needed for Nicolai Kraus example

defCase : (A X:U) -> X -> X -> dec A -> X
defCase A X x0 x1 = 
 split
  inl _ -> x0
  inr _ -> x1

IdDefCasel : (A X:U) (x0 x1 : X) (p : dec A)  -> A -> 
             Id X (defCase A X x0 x1 p) x0
IdDefCasel A X x0 x1 = split
 inl _ -> \ _ -> refl X x0
 inr v -> \ u -> efq (Id X (defCase A X x0 x1 (inr v)) x0) (v u)

IdDefCaser : (A X:U) (x0 x1 : X) (p : dec A)  -> (neg A) -> 
             Id X (defCase A X x0 x1 p) x1
IdDefCaser A X x0 x1 = split
 inl u -> \ v -> efq (Id X (defCase A X x0 x1 (inl u)) x1) (v u)
 inr _ -> \ _ -> refl X x1

-- defines the swap function over a discrete type and proves that this is an involutive 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 = mapOnPath 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 involutive??

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 = mapOnPath 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 (mapOnPath 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 (mapOnPath 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) (mapOnPath X X sD (sD x) (aD x) rem12) (mapOnPath X X sD (aD x) x rem16)

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

-- pointed sets
        
ptU : U
ptU = Sigma U (id U)

-- if f : A -> B is an equivalence and f a = b then (A,a) and (B,b) are equal in ptU

lemPtEquiv : (A B : U) (f: A -> B) (ef: isEquiv A B f) (a:A) (b:B) (eab: Id B (f a) b) 
              -> Id ptU (A,a) (B,b)
lemPtEquiv A = elimIsEquiv A P rem
  where
   P : (B:U) -> (A->B) -> U
   P B f = (a:A) -> (b:B) -> (eab: Id B (f a) b) -> Id ptU (A,a) (B,b)

   rem : P A (id A)
   rem = mapOnPath A ptU (\ x -> (A,x))

homogDec : (X:U) -> discrete X -> (x y:X) -> Id ptU (X,x) (X,y)
homogDec X dX x y = orElim (Id X y x) (neg (Id X y x)) (G x) rem1 rem (dX y x)
 where
   G : X -> U
   G z = Id ptU (X,z) (X,y)

   rem0 : G y
   rem0 = refl ptU (X,y)

   rem : neg (Id X y x) -> G x
   rem neqzx = lemPtEquiv X X (swapDisc X dX y x) 
                (idemIsEquiv X (swapDisc X dX y x) (idemSwapDisc X dX y x neqzx)) 
                x y (idSwapDisc1 X dX y x neqzx)

   rem1 : Id X y x -> G x
   rem1 eqzx = subst X G y x eqzx rem0