monoid.cub

module monoid where
import prelude
import quotient3

MonoidTerm : U -> U
data MonoidTerm A = empty | elem (x:A) | join (x:MonoidTerm A) (y:MonoidTerm A)

emb : (A:U) -> MonoidTerm A -> (MonoidTerm A -> MonoidTerm A)
emb A = split
   empty -> (\x -> x)
   elem t -> (\x -> join (elem t) x)
   join u v -> (\x -> emb A u (emb A v x))


nbe : (A:U) -> MonoidTerm A -> MonoidTerm A
nbe A x = emb A x empty

FreeMonoid : U -> U
FreeMonoid A = 
   quot (MonoidTerm A) (kernel (MonoidTerm A) (MonoidTerm A) (nbe A))


nbe_assoc : 
   (A:U) -> (x y z:MonoidTerm A) -> 
   (Id (MonoidTerm A) (nbe A (join (join x y) z)) (nbe A (join x (join y z))))
nbe_assoc A x y z = refl (MonoidTerm A) (emb A x (emb A y (emb A z empty)))



monoideq : (A:U) -> (x y:MonoidTerm A) -> U
monoideq A x y = (r:rel (MonoidTerm A)) -> (p1:equivalence (MonoidTerm A) r) -> (p2:assocProp r) -> (p3:leftidProp r) -> (p4:rightidProp r) -> (p5:substProp r) -> (r x y)
   where
     assocProp : (r:rel (MonoidTerm A)) -> U
     assocProp r = (x y z:MonoidTerm A) -> (r (join x (join y z)) (join (join x y) z))
     leftidProp : (r:rel (MonoidTerm A)) -> U
     leftidProp r = (x:MonoidTerm A) -> (r (join empty x) x)
     rightidProp : (r:rel (MonoidTerm A)) -> U
     rightidProp r = (x:MonoidTerm A) -> (r (join x empty) x)
     substProp : (r:rel (MonoidTerm A)) -> U
     substProp r = (x1 x2 y1 y2:MonoidTerm A) -> (r x1 x2) -> (r y1 y2) -> (r (join x1 y1) (join x2 y2))


monoideq_refl : (A:U) -> (x:MonoidTerm A) -> monoideq A x x
monoideq_refl A x r p1 p2 p3 p4 p5 = p1.1 x

monoideq_trans : (A:U) -> (x y z:MonoidTerm A) -> (p:monoideq A x z) -> (q:monoideq A y z) -> monoideq A x y
monoideq_trans A x y z p q r p1 p2 p3 p4 p5 = p1.2 x y z (p r p1 p2 p3 p4 p5) (q r p1 p2 p3 p4 p5)


H : (A:U) -> (e e2:MonoidTerm A) -> (monoideq A (join e e2) (emb A e e2))
H A = split
  empty -> (\e2 r p1 p2 p3 p4 p5 -> p3 e2)
  elem x -> (\e2 r p1 p2 p3 p4 p5 -> p1.1 (join (elem x) e2))
  join e0 e1 -> H0
    where
      IH0 : (x:MonoidTerm A) -> (monoideq A (join e0 (emb A e1 x)) (emb A e0 (emb A e1 x)))
      IH0 x = H A e0 (emb A e1 x)
      IH1 : (x:MonoidTerm A) -> (monoideq A (join e1 x) (emb A e1 x))
      IH1 x = H A e1 x
      P0 : monoideq A e0 e0
      P0 r p1 p2 p3 p4 p5 = p1.1 e0
      P1 : (x:MonoidTerm A) -> monoideq A (join e0 (join e1 x)) (join e0 (emb A e1 x))
      P1 x r p1 p2 p3 p4 p5 = p5 e0 e0 (join e1 x) (emb A e1 x) (P0 r p1 p2 p3 p4 p5) (IH1 x r p1 p2 p3 p4 p5)
      P2 : (x:MonoidTerm A) -> (monoideq A (join (join e0 e1) x) (join e0 (join e1 x)))
      P2 x r p1 p2 p3 p4 p5 = 
        eqToSym (MonoidTerm A) r p1 
          (join e0 (join e1 x)) (join (join e0 e1) x) (p2 e0 e1 x)
      P1_rev : (x:MonoidTerm A) -> (monoideq A (join e0 (emb A e1 x)) (join e0 (join e1 x)))
      P1_rev x r p1 p2 p3 p4 p5 = 
        eqToSym (MonoidTerm A) r p1 
          (join e0 (join e1 x)) (join e0 (emb A e1 x)) (P1 x r p1 p2 p3 p4 p5)
      P3 : (x:MonoidTerm A) -> (monoideq A (join (join e0 e1) x) (join e0 (emb A e1 x)))
      P3 x r p1 p2 p3 p4 p5 = 
        p1.2 (join (join e0 e1) x) 
             (join e0 (emb A e1 x)) 
             (join e0 (join e1 x)) 
             (P2 x r p1 p2 p3 p4 p5) 
             (P1_rev x r p1 p2 p3 p4 p5)
      IH0_rev : (x:MonoidTerm A) -> (monoideq A (emb A e0 (emb A e1 x)) (join e0 (emb A e1 x)))
      IH0_rev x r p1 p2 p3 p4 p5 =
        eqToSym (MonoidTerm A) r p1 
          (join e0 (emb A e1 x)) (emb A e0 (emb A e1 x)) 
             (IH0 x r p1 p2 p3 p4 p5)
      H0 : (e2:MonoidTerm A) -> (monoideq A (join (join e0 e1) e2) (emb A e0 (emb A e1 e2)))
      H0 e2 r p1 p2 p3 p4 p5 =
         p1.2 (join (join e0 e1) e2) 
              (emb A e0 (emb A e1 e2))
              (join e0 (emb A e1 e2))
              (P3 e2 r p1 p2 p3 p4 p5)
              (IH0_rev e2 r p1 p2 p3 p4 p5)

-- using H, monoideq A (join e0 empty) (nbe A e0)
-- so,monoideq A e0 (nbe A e0)
-- similarly, monoideq A e1 (nbe A e1)
-- substituting e0 to e1,monoideq A e0 (nbe A e1)
-- by transitivity of monoideq, monoideq A e0 e1
-- nbeToEq : (A:U) -> (e0 e1:MonoidTerm A) -> (h:Id (MonoidTerm A) (nbe e0) (nbe e1)) -> (monoideq A e0 e1)



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


elemInj : (A:U) -> (x y:A) -> (Id (MonoidTerm A) (elem x) (elem y)) -> (Id A x y)
elemInj A x y p = mapOnPath (MonoidTerm A) A f (elem x) (elem y) p
  where
     f : (MonoidTerm A) -> A
     f = split
       empty -> x
       elem a -> a
       join a b -> x

joinproj1 : (A:U) -> (a b c d:MonoidTerm A) -> (Id (MonoidTerm A) (join a b) (join c d)) -> (Id (MonoidTerm A) a c)
joinproj1 A a b c d p = mapOnPath (MonoidTerm A) (MonoidTerm A) f (join a b) (join c d) p
  where
    f : MonoidTerm A -> MonoidTerm A
    f = split
      empty -> empty
      elem u -> empty
      join u v -> u

joinproj2 : (A:U) -> (a b c d:MonoidTerm A) -> (Id (MonoidTerm A) (join a b) (join c d)) -> (Id (MonoidTerm A) b d)
joinproj2 A a b c d p = mapOnPath (MonoidTerm A) (MonoidTerm A) f (join a b) (join c d) p
  where
    f : MonoidTerm A -> MonoidTerm A
    f = split
      empty -> empty
      elem u -> empty
      join u v -> v


joinInj : (A:U) -> (a b c d:MonoidTerm A) -> (Id (MonoidTerm A) (join a b) (join c d)) -> (Id (and (MonoidTerm A) (MonoidTerm A)) (a,b) (c,d))
joinInj A a b c d p = H2
  where
    H0 : Id (and (MonoidTerm A) (MonoidTerm A)) (a,b) (c,b)
    H0 = mapOnPath (MonoidTerm A) (and (MonoidTerm A) (MonoidTerm A)) (\x->(x,b)) a c (joinproj1 A a b c d p)
    H1 : Id (and (MonoidTerm A) (MonoidTerm A)) (c,b) (c,d)
    H1 = mapOnPath (MonoidTerm A) (and (MonoidTerm A) (MonoidTerm A)) (\x->(c,x)) b d (joinproj2 A a b c d p)
    H2 : Id (and (MonoidTerm A) (MonoidTerm A)) (a,b) (c,d)
    H2 = eqtrans (and (MonoidTerm A) (MonoidTerm A)) (a,b) (c,b) (c,d) H0 H1

empty_neq_elem : (A:U) -> (x:A) -> neg (Id (MonoidTerm A) empty (elem x))
empty_neq_elem A x p = subst (MonoidTerm A) f empty (elem x) p x
   where
      f : (MonoidTerm A) -> U
      f = split
        empty -> A
        elem a -> N0
        join a b -> N0


empty_neq_join : (A:U) -> (x y:MonoidTerm A) -> neg (Id (MonoidTerm A) empty (join x y))
empty_neq_join A x y p = subst (MonoidTerm A) f empty (join x y) p empty
  where
     f :(MonoidTerm A) -> U
     f = split
       empty -> (MonoidTerm A)
       elem a -> N0
       join a b -> N0


elem_neq_join : (A:U) -> (x:A) -> (a b:MonoidTerm A) -> neg (Id (MonoidTerm A) (elem x) (join a b))
elem_neq_join A x a b p = subst (MonoidTerm A) f (elem x) (join a b) p empty
   where
     f : MonoidTerm A -> U
     f = split
       empty -> N0
       elem a -> MonoidTerm A
       join p q -> N0


join_neq_elem : (A:U) -> (x:A) -> (a b:MonoidTerm A) -> neg (Id (MonoidTerm A) (join a b) (elem x))
join_neq_elem A x a b p = elem_neq_join A x a b (eqsym (MonoidTerm A) (join a b) (elem x) p)


join_neq_empty : (A:U) -> (x y:MonoidTerm A) -> neg (Id (MonoidTerm A) (join x y) empty)
join_neq_empty A x y p = empty_neq_join A x y (eqsym (MonoidTerm A) (join x y) empty p)


elem_neq_empty : (A:U) -> (x:A) -> neg (Id (MonoidTerm A) (elem x) empty)
elem_neq_empty A x p = empty_neq_elem A x (eqsym (MonoidTerm A) (elem x) empty p)



declift : (A:U) -> (a b c d:MonoidTerm A) -> dec (Id (MonoidTerm A) a c) -> dec (Id (MonoidTerm A) b d) -> dec (Id (and (MonoidTerm A) (MonoidTerm A)) (a,b) (c,d))
declift A a b c d = split
  inl p -> split
     inl q -> inl H0
       where
         P0 : (Id (and (MonoidTerm A) (MonoidTerm A)) (a,b) (c,b))
         P0 = mapOnPath (MonoidTerm A) (and (MonoidTerm A) (MonoidTerm A)) (\x->(x,b)) a c p
         P1 : (Id (and (MonoidTerm A) (MonoidTerm A)) (c,b) (c,d))
         P1 = mapOnPath (MonoidTerm A) (and (MonoidTerm A) (MonoidTerm A)) (\x->(c,x)) b d q
         H0 : (Id (and (MonoidTerm A) (MonoidTerm A)) (a,b) (c,d))
         H0 = eqtrans (and (MonoidTerm A) (MonoidTerm A)) (a,b) (c,b) (c,d) P0 P1
     inr f -> inr H1
       where
         H1: neg (Id (and (MonoidTerm A) (MonoidTerm A)) (a,b) (c,d))
         H1 p = f (mapOnPath (and (MonoidTerm A) (MonoidTerm A)) (MonoidTerm A) (\x->x.2) (a,b) (c,d) p)
  inr g -> (\any -> inr H2)
    where
      H2 : neg (Id (and (MonoidTerm A) (MonoidTerm A)) (a,b) (c,d))
      H2 p = g (mapOnPath (and (MonoidTerm A) (MonoidTerm A)) (MonoidTerm A) (\x->x.1) (a,b) (c,d) p)


eqlift : (A:U) -> (a b c d:MonoidTerm A) -> (Id (and (MonoidTerm A) (MonoidTerm A)) (a,b) (c,d)) -> (Id (MonoidTerm A) (join a b) (join c d))
eqlift A a b c d p = H
  where
    HL : Id (MonoidTerm A) a c
    HL = mapOnPath (and (MonoidTerm A) (MonoidTerm A)) (MonoidTerm A) (\x->x.1) (a,b) (c,d) p
    HR : Id (MonoidTerm A) b d
    HR = mapOnPath (and (MonoidTerm A) (MonoidTerm A)) (MonoidTerm A) (\x->x.2) (a,b) (c,d) p
    P0 : Id (MonoidTerm A) (join a b) (join c b)
    P0 = mapOnPath (MonoidTerm A) (MonoidTerm A) (\x->join x b) a c HL
    P1 : Id (MonoidTerm A) (join c b) (join c d)
    P1 = mapOnPath (MonoidTerm A) (MonoidTerm A) (\x->join c x) b d HR
    H : (Id (MonoidTerm A) (join a b) (join c d))
    H = eqtrans (MonoidTerm A) (join a b) (join c b) (join c d) P0 P1




monoidTermDec : (A:U) -> discrete A -> discrete (MonoidTerm A)
monoidTermDec A decA = split
    empty -> split
      empty -> inl (refl (MonoidTerm A) empty)
      elem x -> inr (empty_neq_elem A x)
      join u v -> inr (empty_neq_join A u v)
    elem x -> split
      empty -> inr (elem_neq_empty A x)
      elem y -> decEqCong (Id A x y) (Id (MonoidTerm A) (elem x) (elem y))
                          (mapOnPath A (MonoidTerm A) (\t->elem t) x y) 
                          (elemInj A x y)
                          (decA x y)
      join u v -> inr (elem_neq_join A x u v)
    join a b -> split
      empty -> inr (join_neq_empty A a b)
      elem x -> inr (join_neq_elem A x a b)
      join c d -> decEqCong (Id (and (MonoidTerm A) (MonoidTerm A)) (a,b) (c,d))
                            (Id (MonoidTerm A) (join a b) (join c d))
                            (eqlift A a b c d)
                            (joinInj A a b c d) 
                            (declift A a b c d (monoidTermDec A decA a c) (monoidTermDec A decA b d))


monoidTermIsSet : (A:U) -> discrete A -> set (MonoidTerm A)
monoidTermIsSet A p = hedberg (MonoidTerm A) (monoidTermDec A p)


propMonoidEq : (A:U) -> discrete A -> propRel (MonoidTerm A) (kernel (MonoidTerm A) (MonoidTerm A) (nbe A))
propMonoidEq A p x y = monoidTermIsSet A p (nbe A x) (nbe A y)