module swapDisc where

import lemId
import involutive
import contr
import elimEquiv

-- defines the swap function over a discrete type and proves that this is an involutive map
-- needed for Nicolai Kraus example
-- we try another representation since the other one is too slow

if : (X:U) -> Bool -> X -> X -> X
if X = split true -> \ x y -> x
             false -> \ x y -> y

True : Bool -> U
True = split true -> Unit
             false -> N0

lemIfT : (X:U) (b:Bool) (x y:X) -> True b -> Id X (if X b x y) x
lemIfT X = split true -> \ x y _ -> refl X x
                 false -> \ x y h -> efq (Id X (if X false x y) x) h

lemIfF : (X:U) (b:Bool) (x y:X) -> True (not b) -> Id X (if X b x y) y
lemIfF X = split true -> \ x y h -> efq (Id X (if X true x y) y) h
                 false -> \ x y _ -> refl X y

lemTrue : (a b : Bool) ->
            or (True a)
               (or (and (True (not a)) (True b)) (and (True (not a)) (True (not b))))
lemTrue = split true -> \ b -> inl tt
                false -> split true -> inr (inl (tt,tt))
                               false -> inr (inr (tt,tt))

lemTrue : (a b : Bool) (G:U) ->
            ((True a) -> G) -> ((and (True (not a)) (True b)) -> G) ->
            ((and (True (not a)) (True (not b)))-> G) -> G
lemTrue = split true -> \ b -> \ G h0 h1 h2 -> h0 tt
                false -> split true -> \ G h0 h1 h2 -> h1 (tt,tt)
                               false -> \ G h0 h1 h2 -> h2 (tt,tt)


swapF : (X:U) (eq:X->X-> Bool) -> X -> X -> X -> X
swapF X eq x y u = if X (eq x u) y (if X (eq y u) x u)

lemSw0 : (X:U) (eq:X->X->Bool) (x y u:X) -> True (eq x u) -> Id X (swapF X eq x y u) y
lemSw0 X eq x y u h = lemIfT X (eq x u) y (if X (eq y u) x u) h

lemSw1 : (X:U) (eq:X->X->Bool) (x y u:X) ->
               and (True (not (eq x u))) (True (eq y u)) -> Id X (swapF X eq x y u) x
lemSw1 X eq x y u h = comp X (swapF X eq x y u) (if X (eq y u) x u) x rem rem1
   where rem : Id X (swapF X eq x y u) (if X (eq y u) x u)
         rem = lemIfF X (eq x u) y (if X (eq y u) x u) h.1
         rem1 : Id X (if X (eq y u) x u) x
         rem1 = lemIfT X (eq y u) x u h.2

lemSw2 : (X:U) (eq:X->X->Bool) (x y u:X) ->
               and (True (not (eq x u))) (True (not (eq y u)))
          -> Id X (swapF X eq x y u) u
lemSw2 X eq x y u h = comp X (swapF X eq x y u) (if X (eq y u) x u) u rem rem1
   where rem : Id X (swapF X eq x y u) (if X (eq y u) x u)
         rem = lemIfF X (eq x u) y (if X (eq y u) x u) h.1
         rem1 : Id X (if X (eq y u) x u) u
         rem1 = lemIfF X (eq y u) x u h.2

faith0 : (X:U) (eq:X->X->Bool) -> U
faith0 X eq = (x y : X) -> Id X x y -> True (eq x y)

faith1 : (X:U) (eq:X->X->Bool) -> U
faith1 X eq = (x y : X) -> True (eq x y) -> Id X x y

lemIdemSw : (X:U) (eq:X->X->Bool) (f0:faith0 X eq) (f1:faith1 X eq) (x y : X) (neq : True (not (eq x y)))
            (u:X) -> Id X (swapF X eq x y (swapF X eq x y u)) u
lemIdemSw X eq f0 f1 x y neq u = lemTrue (eq x u) (eq y u) (H u) rem5 rem6 rem7
 where
   sw : X -> X
   sw = swapF X eq x y

   H : X -> U
   H v = Id X (sw (sw v)) v

   rem1 : Id X (sw x) y
   rem1 = lemSw0 X eq x y x (f0 x x (refl X x))

   rem2 : Id X (sw y) x
   rem2 = lemSw1 X eq x y y (neq,f0 y y (refl X y))

   rem3 : H x
   rem3 = comp X (sw (sw x)) (sw y) x (mapOnPath X X sw (sw x) y rem1) rem2

   rem4 : H y
   rem4 = comp X (sw (sw y)) (sw x) y (mapOnPath X X sw (sw y) x rem2) rem1

   rem5 : True (eq x u) -> H u
   rem5 h = subst X H x u (f1 x u h) rem3

   rem6 : and (True (not (eq x u))) (True (eq y u)) -> H u
   rem6 h = subst X H y u (f1 y u h.2) rem4

   rem7 : and (True (not (eq x u))) (True (not (eq y u))) -> H u
   rem7 h = comp X (sw (sw u)) (sw u) u (mapOnPath X X sw (sw u) u lem) lem
     where lem : Id X (sw u) u
           lem = lemSw2 X eq x y u h

-- 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))


lemEM : (b:Bool) (G:U) -> ((True b) -> G) -> ((True (not b)) -> G) -> G
lemEM = split true -> \ G h0 h1 -> h0 tt
              false -> \ G h0 h1 -> h1 tt

homogDec : (X:U) (eq:X->X->Bool) (f0:faith0 X eq) (f1:faith1 X eq) (x y : X)
           -> Id ptU (X,x) (X,y)
homogDec X eq f0 f1 x y = lemEM (eq x y) (G y) rem1 rem
 where
   G : X -> U
   G z = Id ptU (X,x) (X,z)

   sw : X -> X
   sw = swapF X eq x y

   rem : True (not (eq x y)) -> G y
   rem neq = lemPtEquiv X X sw
                (idemIsEquiv X sw (lemIdemSw X eq f0 f1 x y neq))
                x y (lemSw0 X eq x y x (f0 x x (refl X x)))

   rem1 : True (eq x y) -> G y
   rem1 h = subst X G x y (f1 x y h) (refl ptU (X,x))


-- an example of a decidable structure

eqN : N -> N -> Bool
eqN = split zero -> split
                      zero -> true
                      suc _ -> false
            suc n -> split
                      zero -> false
                      suc m -> eqN n m

lemN : (x:N) -> True (eqN x x)
lemN = split
        zero -> tt
        suc n -> lemN n

f0N : (x y : N) -> Id N x y -> True (eqN x y)
f0N x y p = subst N (\ y -> True (eqN x y)) x y p (lemN x)

f1N : (x y : N) -> True (eqN x y) -> Id N x y
f1N =  split zero -> split
                      zero -> \ _ ->refl N zero
                      suc m -> \ h -> efq (Id N zero (suc m)) h
             suc n -> split
                       zero ->  \ h -> efq (Id N (suc n) zero) h
                       suc m -> \ h -> mapOnPath N N (\ x -> suc x) n m (f1N n m h)