module finite where

-- definition of finite sets and cardinality

import description
import function
import gradLemma
import swapDisc_old

step : U -> U
step X = or Unit X

incSt : (X:U) -> X -> step X
incSt X x = inr x

injSt : (X:U) -> injective X (step X) (incSt X)
injSt X x0 x1 h = subst (step X) T (inr x0) (inr x1) h (refl X x0)
 where
   T : step X -> U
   T = split
         inl _ -> N0
         inr x -> Id X x0 x

incUnSt : (X:U) -> Unit -> step X
incUnSt X x = inl x

inlNotinr : (A B:U) (a:A) (b:B) -> neg (Id (or A B) (inl a) (inr b))
inlNotinr A B a b h = subst (or A B) T (inl a) (inr b) h tt
 where
  T : or A B -> U
  T = split
       inl _ -> Unit
       inr _ -> N0

inrNotinl : (A B:U) (a:A) (b:B) -> neg (Id (or A B) (inr b) (inl a))
inrNotinl A B a b h = subst (or A B) T (inr b) (inl a) h tt
 where
  T : or A B -> U
  T = split
       inl _ -> N0
       inr _ -> Unit

decSt : (X:U) -> discrete X -> discrete (step X)
decSt X dX =
 split
  inl a -> split
            inl a1 -> inl (mapOnPath Unit (step X) (incUnSt X) a a1 (propUnit a a1))
            inr b -> inr (inlNotinr Unit X a b)
  inr b -> split
            inl a -> inr (inrNotinl Unit X a b)
            inr b1 -> rem (dX b b1)
               where rem : dec (Id X b b1) -> dec (Id (step X) (inr b) (inr b1))
                     rem = split
                            inl p -> inl (mapOnPath X (step X) (incSt X) b b1 p)
                            inr h -> inr (\ p -> h (injSt X b b1 p))

stFin : N -> U
stFin = split
         zero -> N0
         suc n -> step (stFin n)

lemN0 : (X:U) -> Id U (or X N0) X
lemN0 X = isEquivEq (or X N0) X f ef
 where
  f : or X N0 -> X
  f = split
        inl x -> x
        inr y -> efq X y

  g : X -> or X N0
  g x = inl x

  sfg : (z:or X N0) -> Id (or X N0) (g (f z)) z
  sfg = split
         inl x -> refl (or X N0) (inl x)
         inr y -> efq (Id (or X N0) (g (f (inr y))) (inr y)) y

  rfg : (x:X) -> Id X (f (g x)) x
  rfg x = refl X x

  ef : isEquiv (or X N0) X f
  ef = gradLemma (or X N0) X f g rfg sfg

N0Dec : discrete N0
N0Dec = \ x y -> efq (dec (Id N0 x y)) x

finDec : (n:N) -> discrete (stFin n)
finDec = split
          zero -> N0Dec
          suc m -> decSt (stFin m) (finDec m)

unitDec : discrete Unit
unitDec = split
           tt -> split
                  tt -> inl (refl Unit tt)

-- take away one element

takeAway : (A:U) -> A -> U
takeAway A a = Sigma A (\ x -> neg (Id A a x))

tAway : ptU -> U
tAway z = takeAway z.1 z.2

-- this has been generalized from a special case

eqTkA : (X:U) -> Id U (takeAway (step X) (inl tt)) X
eqTkA X = isEquivEq tS X f equivf
 where
   stS : U
   stS = step X

   bn : stS
   bn = inl tt

   tS : U
   tS = takeAway stS bn

   faux : (x:stS) -> neg (Id stS bn x) -> X
   faux = split
            inl u -> \ h -> efq X (h rem)
              where rem : Id stS bn (inl u)
                    rem = mapOnPath Unit stS (incUnSt X) tt u (propUnit tt u)
            inr z -> \ _ -> z

   f : tS -> X
   f z = faux z.1 z.2

   lem : (x:X) -> neg (Id stS bn (inr x))
   lem x = inlNotinr Unit X tt x

   g : X -> tS
   g x = (inr x,lem x)

   T : stS -> U
   T x = neg (Id stS bn x)

   lem1 : (u:Unit) -> Id stS bn (inl u)
   lem1 u = mapOnPath Unit stS (incUnSt X) tt u (propUnit tt u)

   lem2 : propFam stS T
   lem2 = \ x -> propNeg (Id stS bn x)

   sfg : (x:X) -> Id X (f (g x)) x
   sfg x = refl X x

   rfg : (z:tS) -> Id tS (g (f z)) z
   rfg z = rem z.1 z.2
            where rem : (x:stS) -> (p : T x) -> Id tS (g (f (x,p))) (x,p)
                  rem = split
                   inl u -> \ h -> efq (Id tS (g (f (inl u,h))) (inl u,h)) (h (lem1 u))
                   inr z -> \ h -> eqPropFam stS T lem2
                                    (inr z,lem (faux (inr z) h)) (inr z,h) (refl stS (inr z))

   equivf : isEquiv tS X f
   equivf = gradLemma tS X f g sfg rfg

botEl : (n:N) -> stFin (suc n)
botEl n = inl tt

ptBot : N -> ptU
ptBot n = (stFin (suc n),botEl n)

mkPtU : (n:N) (x:stFin (suc n)) -> ptU
mkPtU n x = (stFin (suc n),x)

homogSt : (X:U) -> discrete X -> (x:step X) -> Id ptU (step X,x) (step X,inl tt)
homogSt X dX x = homogDec (step X) (decSt X dX) x (inl tt)

corHomogSt : (X:U) -> discrete X -> (x:step X) -> Id U (takeAway (step X) x) X
corHomogSt X dX x =
 substInv ptU (\ z -> Id U (tAway z) X) (step X,x) (step X,inl tt)
    (homogSt X dX x) (eqTkA X)

-- eqTkA : (X:U) -> Id U (takeAway (step X) (inl tt)) X

homogSt' : (n:N) (x:stFin (suc n)) -> Id ptU (mkPtU n x) (ptBot n)
homogSt' n = homogSt (stFin n) (finDec n)

corEqTkA : (n:N) -> Id U (tAway (ptBot n)) (stFin n)
corEqTkA n = eqTkA (stFin n)

cor1EqTkA : (n:N) (x:stFin (suc n)) -> Id U (tAway (mkPtU n x)) (stFin n)
cor1EqTkA n x =
 substInv ptU (\ z -> Id U (tAway z) (stFin n)) (mkPtU n x) (ptBot n) (homogSt' n x) (corEqTkA n)

lemInjSt : (X Y:U) -> discrete X -> Id U (step X) (step Y) -> Id U X Y
lemInjSt X Y dX h = lem5
 where
  P : U -> U
  P Z = (x:Z) -> Id U (takeAway Z x) X

  lem1 : P (step X)
  lem1 = corHomogSt X dX

  lem2 : P (step Y)
  lem2 = subst U P (step X) (step Y) h lem1

  Am : U
  Am = takeAway (step Y) (inl tt)

  lem3 : Id U Am Y
  lem3 = eqTkA Y

  lem4 : Id U Am X
  lem4 = lem2 (inl tt)

  lem5 : Id U X Y
  lem5 = comp U X Am Y (inv U Am X lem4) lem3

lem1InjSt : (n:N) -> neg (Id U N0 (stFin (suc n)))
lem1InjSt n h = transportInv N0 (stFin (suc n)) h (botEl n)

lem2InjSt : (n:N) -> neg (Id U (stFin (suc n)) N0)
lem2InjSt n h = transport (stFin (suc n)) N0 h (botEl n)

lemInj : injective N U stFin
lemInj = split
           zero -> split
                    zero -> \ _ -> refl N zero
                    suc m -> \ h -> efq (Id N zero (suc m)) (lem1InjSt m h)
           suc n -> split
                     zero -> \ h -> efq (Id N (suc n) zero) (lem2InjSt n h)
                     suc m -> \ h ->
                       mapOnPath N N (\ x -> suc x) n m (lemInj n m (lemInjSt (stFin n) (stFin m) (finDec n) h))

eqsT : U -> N -> U
eqsT X n = inh (Id U (stFin n) X)

finite : U -> U
finite X = exists N (eqsT X)

lemEqsT : (X:U) (n m:N) -> eqsT X n -> eqsT X m -> Id N n m
lemEqsT X n m = rem2
 where
  G : U
  G = Id N n m

  pG : prop G
  pG = NIsSet n m

  rem : Id U (stFin n) X -> Id U (stFin m) X -> G
  rem ln lm = lemInj n m (comp U (stFin n) X (stFin m) ln (inv U (stFin m) X lm))

  rem1 : Id U (stFin n) X -> eqsT X m -> G
  rem1 ln = inhrec (Id U (stFin m) X) G pG (rem ln)

  rem2 : eqsT X n -> eqsT X m -> G
  rem2 hn hm = inhrec (Id U (stFin n) X) G pG (\ l -> rem1 l hm) hn

propEqsT : (X:U) -> prop (Sigma N (eqsT X))
propEqsT X = propSig N (eqsT X) (\ n -> squash (Id U (stFin n) X)) rem
 where rem : atmostOne N (eqsT X)
       rem = lemEqsT X

cardFin : (X:U) -> finite X -> Sigma N (eqsT X)
cardFin X = inhrec (Sigma N (eqsT X)) (Sigma N (eqsT X)) (propEqsT X) (\ h -> h)

-- Unit is finite

finUnit : finite Unit
finUnit = inc (Sigma N (eqsT Unit)) rem
 where rem : Sigma N (eqsT Unit)
       rem = (suc zero,inc (Id U (stFin (suc zero)) Unit) (lemN0 Unit))

       rem1 : Id U (stFin (suc zero)) Unit
       rem1 = lemN0 Unit

test : N
test = (cardFin Unit finUnit).1