module finite where

-- definition of finite sets and cardinality 

import description
import function 
import gradLemma
import Kraus

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


isolated : (A:U) -> A -> U
isolated A a = (x:A) -> dec (Id A a x)

-- take away one element

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

tAway : ptU -> U
tAway = split
         pair A a -> takeAway A a

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

eqTkA : (n:N) -> Id U (takeAway (stFin (suc n)) (botEl n)) (stFin n)
eqTkA n = isEquivEq tS (stFin n) f equivf
 where
   stS : U
   stS = stFin (suc n)

   bn : stS
   bn = botEl n

   tS : U
   tS = takeAway stS bn

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

   f : tS -> stFin n
   f = split
        pair x p -> faux x p

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

   g : stFin n -> tS
   g x = pair (inr x) (lem x)

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

   lem1 : (u:Unit) -> Id stS bn (inl u)
   lem1 u = cong Unit stS (incUnSt (stFin n)) tt u (propUnit tt u)

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

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

   rfg : (z:tS) -> Id tS (g (f z)) z
   rfg = split
          pair x p -> rem x p
            where rem : (x:stS) -> (p : T x) -> Id tS (g (f (pair x p))) (pair x p)
                  rem = split
                   inl u -> \ h -> efq (Id tS (g (f (pair (inl u) h))) (pair (inl u) h)) (h (lem1 u))
                   inr z -> \ h -> eqPropFam stS T lem2
                                    (pair (inr z) (lem (faux (inr z) h))) (pair (inr z) h) (refl stS (inr z))
  
   equivf : isEquiv tS (stFin n) f 
   equivf = gradLemma tS (stFin n) f g sfg rfg
 
-- Pointed set with one isolated element

hasPointIso : U -> U
hasPointIso A = Sigma A (isolated A)
ptBot : N -> ptU
ptBot n = pair (stFin (suc n)) (botEl n)

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

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

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

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 : (n m:N) -> Id U (stFin (suc n)) (stFin (suc m)) -> Id U (stFin n) (stFin m)
lemInjSt n m h = lem5
 where
  P : U -> U
  P X = (x:X) -> Id U (takeAway X x) (stFin n)

  lem1 : P (stFin (suc n))
  lem1 = cor1EqTkA n

  lem2 : P (stFin (suc m))
  lem2 = subst U P (stFin (suc n)) (stFin (suc m)) h lem1

  Am : U
  Am = takeAway (stFin (suc m)) (botEl m)

  lem3 : Id U Am (stFin m)
  lem3 = cor1EqTkA m (botEl m)

  lem4 : Id U Am (stFin n)
  lem4 = lem2 (botEl m)

  lem5 : Id U (stFin n) (stFin m)
  lem5 = comp U (stFin n) Am (stFin m) (inv U Am (stFin n) 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 -> cong N N (\ x -> suc x) n m (lemInj n m (lemInjSt n m 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 = pair (suc zero) (inc (Id U (stFin (suc zero)) Unit) (lemN0 Unit))

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

test : N
test = fst N (eqsT Unit) (cardFin Unit finUnit)