uarith.cub

----------------------------------------------
-- implementation of "arithmetic via univalence"
-- https://groups.google.com/forum/#!topic/homotopytypetheory/n13Gh2GGe0g
--
-- written in the cubical type theory
-- https://github.com/simhu/cubical
----------------------------------------------
module uarith where
import finite
import swap


eqsym : (X:U) -> (x y:X) -> Id X x y -> Id X y x
eqsym X x y p = subst X (\z -> Id X z x) x y p (refl X x)

eqtrans : (X:U) -> (x y z:X) -> Id X x y -> Id X y z -> Id X x z
eqtrans X x y z p q = subst X (\c -> Id X c z) y x (eqsym X x y p) q


-- X = X + 0
uni_p_0 : (X:U) -> Id U X (or X N0)
uni_p_0 X = eqsym U (or X N0) X (lemN0 X)


-- (X + Y) + 1 = X + (Y + 1)
uni_p_1 : (X Y:U) -> Id U (or (or X Y) Unit) (or X (or Y Unit))
uni_p_1 X Y = isEquivEq (or (or X Y) Unit) (or X (or Y Unit)) f ef
  where
    f : or (or X Y) Unit -> or X (or Y Unit)
    f = split
          inl c -> pf c
            where pf : or X Y -> or X (or Y Unit)
                  pf = split
                         inl x -> inl x
                         inr y -> inr (inl y)
          inr u -> inr (inr u)
    g : or X (or Y Unit) -> or (or X Y) Unit
    g = split
          inl x -> inl (inl x)
          inr c -> pg c
            where pg : (or Y Unit) -> or (or X Y) Unit
                  pg = split
                         inl y -> inl (inr y)
                         inr u -> inr u
    psfg : (x:or X Y) -> Id (or (or X Y) Unit) (g (f (inl x))) (inl x)
    psfg = split
             inl b -> refl (or (or X Y) Unit) (inl (inl b))
             inr b -> refl (or (or X Y) Unit) (inl (inr b))
    sfg : (z:or (or X Y) Unit) -> Id (or (or X Y) Unit) (g (f z)) z
    sfg = split
            inl a -> psfg a
            inr a -> refl (or (or X Y) Unit) (inr a)
    prfg : (x:or Y Unit) -> Id (or X (or Y Unit)) (f (g (inr x))) (inr x)
    prfg = split 
             inl b -> refl (or X (or Y Unit)) (inr (inl b))
             inr b -> refl (or X (or Y Unit)) (inr (inr b))
    rfg : (z:or X (or Y Unit)) -> Id (or X (or Y Unit)) (f (g z)) z
    rfg  = split
             inl x -> refl (or X (or Y Unit)) (inl x)
             inr yu -> prfg yu
    ef : isEquiv (or (or X Y) Unit) (or X (or Y Unit)) f
    ef = gradLemma (or (or X Y) Unit) (or X (or Y Unit)) f g rfg sfg


-- X + Y = Y + X
uni_p_comm : (X Y:U) -> Id U (or X Y) (or Y X)
uni_p_comm X Y = isEquivEq (or X Y) (or Y X) f ef
   where
      f : (or X Y) -> (or Y X)
      f = split
           inl a -> inr a
           inr b -> inl b
      g : (or Y X) -> (or X Y)
      g = split
           inl a -> inr a
           inr b -> inl b
      sfg : (z:or X Y) -> Id (or X Y) (g (f z)) z
      sfg = split
         inl a -> refl (or X Y) (inl a)
         inr b -> refl (or X Y) (inr b)
      rfg : (z:or Y X) -> Id (or Y X) (f (g z)) z
      rfg = split
         inl a -> refl (or Y X) (inl a)
         inr b -> refl (or Y X) (inr b)
      ef : isEquiv (or X Y) (or Y X) f
      ef = gradLemma (or X Y) (or Y X) f g rfg sfg



-- X x Y = Y x X
uni_x_comm : (X Y:U) -> Id U (and X Y) (and Y X) 
uni_x_comm X Y = isEquivEq (and X Y) (and Y X) f ef
   where
      f : (and X Y) -> (and Y X)
      f = swap X Y
      g : (and Y X) -> (and X Y)
      g = swap Y X
      sfg : (z:and X Y) -> Id (and X Y) (g (f z)) z
      sfg z = refl (and X Y) z
      rfg : (z:and Y X) -> Id (and Y X) (f (g z)) z
      rfg z = refl (and Y X) z
      ef : isEquiv (and X Y) (and Y X) f
      ef = gradLemma (and X Y) (and Y X) f g rfg sfg


-- X x Y + X = X x (Y + 1)
uni_distr : (X Y :U) -> Id U (or (and X Y) X) (and X (or Y Unit))
uni_distr X Y = isEquivEq (or (and X Y) X) (and X (or Y Unit)) f ef
   where
       f : (or (and X Y) X) -> (and X (or Y Unit))
       f = split
             inl z -> (z.1 , inl z.2)
             inr x -> (x , inr tt)
       pg : X -> (or Y Unit) -> (or (and X Y) X)
       pg x = split
                inl y -> inl (x,y)
                inr u -> inr x
       g : (and X (or Y Unit)) -> (or (and X Y) X)
       g z = pg (z.1) (z.2)
       sfg : (z:or (and X Y) X) -> Id (or (and X Y) X) (g (f z)) z
       sfg = split
               inl xy -> refl (or (and X Y) X) (inl xy)
               inr x -> refl (or (and X Y) X) (inr x)
       prfg : (a:X) -> (b:or Y Unit) -> Id (and X (or Y Unit)) (f (g (a,b))) (a,b)
       prfg a = 
         split
           inl y -> refl (and X (or Y Unit)) (a,inl y)
           inr u -> subst Unit p tt u (uu u) (refl (and X (or Y Unit)) (a,inr tt))
               where p : (x:Unit) -> U
                     p x = Id (and X (or Y Unit)) (a,inr tt) (a,inr x)
                     uu : (x:Unit) -> Id Unit tt x
                     uu = split
                            tt -> refl Unit tt
       rfg : (z:and X (or Y Unit)) -> Id (and X (or Y Unit)) (f (g z)) z
       rfg z = prfg (z.1) (z.2)
       ef : isEquiv (or (and X Y) X) (and X (or Y Unit)) f
       ef = gradLemma (or (and X Y) X) (and X (or Y Unit)) f g rfg sfg


-- 0 = X x 0
unit_x_0 : (X:U) -> Id U N0 (and X N0)
unit_x_0 X = isEquivEq N0 (and X N0) f ef
   where
      f : N0 -> (and X N0)
      f = efq (and X N0)
      g : (and X N0) -> N0
      g x = efq N0 (x.2)
      sfg : (z:N0) -> Id N0 (g (f z)) z
      sfg z = efq (Id N0 (g (f z)) z) z
      rfg : (z:and X N0) -> Id (and X N0) (f (g z)) z
      rfg z = efq (Id (and X N0) (f (g z)) z) (z.2)
      ef : isEquiv N0 (and X N0) f
      ef = gradLemma N0 (and X N0) f g rfg sfg



plusN : N -> N -> N
plusN m = split
   zero -> m
   suc x -> suc (plusN m x)


-- stFin (m + n) = stFin m + stFin n
Fin_p_homo : (m n:N) -> Id U (stFin (plusN m n)) (or (stFin m) (stFin n))
Fin_p_homo m = split
   zero -> uni_p_0 (stFin m)
   suc x -> q3
      where
         IH : Id U (stFin (plusN m x)) (or (stFin m) (stFin x))
         IH = Fin_p_homo m x
         p : Id U (or (stFin (plusN m x)) Unit) (or (or (stFin m) (stFin x)) Unit)
         p = mapOnPath U U (\x -> or x Unit) (stFin (plusN m x)) (or (stFin m) (stFin x)) IH
         p2 : Id U (or (or (stFin m) (stFin x)) Unit) (or (stFin m) (or (stFin x) Unit))
         p2 = uni_p_1 (stFin m) (stFin x)
         p3 : Id U (step (stFin (plusN m x))) (or (stFin (plusN m x)) Unit)
         p3 = uni_p_comm Unit (stFin (plusN m x))
         p4 : Id U (or (stFin m) (or (stFin x) Unit)) (or (stFin m) (step (stFin x)))
         p4 = mapOnPath U U (\c -> (or (stFin m) c)) (or (stFin x) Unit) (step (stFin x)) (uni_p_comm (stFin x) Unit)
         q1 : Id U (step (stFin (plusN m x))) (or (or (stFin m) (stFin x)) Unit)
         q1 = eqtrans U (step (stFin (plusN m x))) (or (stFin (plusN m x)) Unit) (or (or (stFin m) (stFin x)) Unit) p3 p
         q2 : Id U (step (stFin (plusN m x))) (or (stFin m) (or (stFin x) Unit))
         q2 = eqtrans U (step (stFin (plusN m x))) (or (or (stFin m) (stFin x)) Unit) (or (stFin m) (or (stFin x) Unit)) q1 p2
         q3 : Id U (step (stFin (plusN m x))) (or (stFin m) (step (stFin x)))
         q3 = eqtrans U (step (stFin (plusN m x))) (or (stFin m) (or (stFin x) Unit)) (or (stFin m) (step (stFin x))) q2 p4


mulN : N -> N -> N
mulN m = split
   zero -> zero
   suc x -> plusN (mulN m x) m


--  stFin(X x Y) = stFin(X) x stFin(Y)
Fin_x_homo : (m n:N) -> Id U (stFin (mulN m n)) (and (stFin m) (stFin n))
Fin_x_homo m = split
   zero -> unit_x_0 (stFin m)
   suc x -> q3
     where
        p1 : Id U (stFin (mulN m (suc x))) (or (stFin (mulN m x)) (stFin m))
        p1 = Fin_p_homo (mulN m x) m
        IH : Id U (stFin (mulN m x)) (and (stFin m) (stFin x))
        IH = Fin_x_homo m x
        p2 : Id U (or (stFin (mulN m x)) (stFin m)) (or (and (stFin m) (stFin x)) (stFin m))
        p2 = mapOnPath U U (\c -> or c (stFin m)) (stFin (mulN m x)) (and (stFin m) (stFin x)) IH
        p3 : Id U (or (and (stFin m) (stFin x)) (stFin m)) (and (stFin m) (or (stFin x) Unit))
        p3 = uni_distr (stFin m) (stFin x)
        p4 : Id U (and (stFin m) (or (stFin x) Unit)) (and (stFin m) (or Unit (stFin x)))
        p4 = mapOnPath U U (\c->and (stFin m) c) (or (stFin x) Unit) (or Unit (stFin x)) (uni_p_comm (stFin x) Unit)
        q1 : Id U (stFin (mulN m (suc x))) (or (and (stFin m) (stFin x)) (stFin m))
        q1 = eqtrans U (stFin (mulN m (suc x))) (or (stFin (mulN m x)) (stFin m)) (or (and (stFin m) (stFin x)) (stFin m)) p1 p2
        q2 : Id U (stFin (mulN m (suc x))) (and (stFin m) (or (stFin x) Unit))
        q2 = eqtrans U (stFin (mulN m (suc x))) (or (and (stFin m) (stFin x)) (stFin m)) (and (stFin m) (or (stFin x) Unit)) q1 p3
        q3 : Id U (stFin (mulN m (suc x))) (and (stFin m) (or Unit (stFin x)))
        q3 = eqtrans U (stFin (mulN m (suc x))) (and (stFin m) (or (stFin x) Unit)) (and (stFin m) (or Unit (stFin x))) q2 p4




projl : (m n:N) -> stFin (mulN m n) -> stFin m
projl m n x = pi1 (transport (stFin (mulN m n)) (and (stFin m) (stFin n)) (Fin_x_homo m n) x)
   where pi1 : and (stFin m) (stFin n) -> stFin m
         pi1 z = z.1

projr : (m n:N) -> stFin (mulN m n) -> stFin n
projr m n x = pi2 (transport (stFin (mulN m n)) (and (stFin m) (stFin n)) (Fin_x_homo m n) x)
   where pi2 : and (stFin m) (stFin n) -> stFin n
         pi2 z = z.2

--------
-- test
--------
one : N
one = suc zero
two:N
two = suc one
three : N
three = suc two
four : N
four = suc three
five : N
five = suc four
six : N
six = suc five
seven : N
seven = suc six
eight : N
eight = suc seven


one_in_one : stFin one
one_in_one = inl tt

one_in_two : stFin two
one_in_two = inl tt

two_in_two : stFin two
two_in_two = inr (inl tt)

one_in_three : stFin three
one_in_three = inl tt

three_in_three : stFin three
three_in_three = inr (inr (inl tt))

three_in_four : stFin four
three_in_four = inr (inr (inl tt))

three_in_six : stFin six
three_in_six = inr (inr (inl tt))

four_in_eight : stFin eight
four_in_eight = inr (inr (inr (inl tt)))

five_in_eight : stFin eight
five_in_eight = inr (inr (inr (inr (inl tt))))

test1 : stFin two
test1 = projl two two three_in_four

test2 : stFin two
test2 = projr two two three_in_four

test3 : stFin two
test3 = projl two three three_in_six

test4 : stFin two
test4 = projl two four four_in_eight

test5 : stFin four
test5 = projl four two five_in_eight