\import Algebra.Algebra
\import Algebra.Group
\import Algebra.Group.Category
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Pointed
\import Algebra.Pointed.Category
\import Algebra.Ring
\import Algebra.Ring.Category
\import Algebra.Ring.RingHom
\import Algebra.Ring.Poly
\import Algebra.Semiring
\import Category
\import Data.Array
\import Data.Or
\import Equiv (Equiv)
\import Function (isInj)
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence \hiding (~)
\import Set
\import Set.Fin
\import Set.Fin.KFin
\open EPerm
\open Transitive(Closure,cin,ctrans)
\open AddMonoid

\type MonoidSet (M : \Set) (R : AddMonoid) => Quotient {Array (\Sigma R M)} (~)
  \where {
    \data \infix  ~ {M : \Set} {R : AddMonoid} (l l' : Array (\Sigma R M))
      | ~-perm (EPerm l l')
      | ~-sym (l' ~ l)
      | ~-zro {m : M} (l = (,m) :: l')
      | ~-+ {l'' : Array (\Sigma R M)} (m : M) {a b : R} (l = (a + b, m) :: l'') (l' = (a,m) :: (b,m) :: l'')

    \func inMS~ {M : \Set} {R : AddMonoid} (l : Array (\Sigma R M)) : Quotient (~) => in~ l

    \func inMS {M : \Set} {R : AddMonoid} (l : Array (\Sigma R M)) : MonoidSet M R => in~ l

    \lemma ~-msequiv {M : \Set} {R : AddMonoid} {l l' : Array (\Sigma R M)} (p : l ~ l') : inMS l = inMS l'
      => path \lam i => ~-pequiv p i

    \func ~_++-left {M : \Set} {R : AddMonoid} {l1 l2 l : Array (\Sigma R M)} (e : l1 ~ l2) : (l1 ++ l) ~ (l2 ++ l) \elim e
      | ~-perm e => ~-perm (eperm-++-left e)
      | ~-sym e => ~-sym (~_++-left e)
      | ~-zro p => ~-zro (pmap (`++ l) p)
      | ~-+ m p q => ~-+ m (pmap (`++ l) p) (pmap (`++ l) q)

    \lemma ~_++-right {M : \Set} {R : AddMonoid} {l l1 l2 : Array (\Sigma R M)} (e : Closure (~) l1 l2) : Closure (~) (l ++ l1) (l ++ l2) \elim e
      | cin e => cin (~-perm eperm-++-comm) `ctrans` cin (~_++-left e) `ctrans` cin (~-perm eperm-++-comm)
      | ctrans e1 e2 => ~_++-right e1 `ctrans` ~_++-right e2

    \lemma ~_++ {M : \Set} {R : AddMonoid} {l1 l2 l1' l2' : Array (\Sigma R M)} (e1 : Closure (~) l1 l1') (e2 : Closure (~) l2 l2') : Closure (~) (l1 ++ l2) (l1' ++ l2') \elim e1
      | cin e1 => cin (~_++-left e1) `ctrans` ~_++-right e2
      | ctrans r1 r2 => ~_++ r1 e2 `ctrans` ~_++ r2 (cin (~-perm eperm-refl))

    \lemma ~_Big++ {M : \Set} {R : AddMonoid} {n : Nat} {ls ls' : Array (Array (\Sigma R M)) n} (es : \Pi (j : Fin n) -> Closure (~) (ls j) (ls' j)) : Closure (~) (Big (++) nil ls) (Big (++) nil ls') \elim n, ls, ls'
      | , nil, nil => cin (~-perm eperm-refl)
      | suc n, l :: ls, l' :: ls' => ~_++ (es ) $ ~_Big++ \lam j => es (suc j)

    \func ~_map {M M' : \Set} (f : AddMonoidHom) (g : M -> M') {l l' : Array (\Sigma f.Dom M)} (e : l ~ l') : map (\lam s => (f s., g s.)) l ~ map (\lam s => (f s., g s.)) l' \elim e
      | ~-perm e => ~-perm (EPerm_map (\lam s => (f s., g s.)) e)
      | ~-sym e => ~-sym (~_map f g e)
      | ~-zro {m} idp => ~-zro $ pmap (\lam x => (x, g m) :: map (\lam s => (f s., g s.)) l') f.func-zro
      | ~-+ {l''} m idp idp => ~-+ (g m) (pmap (\lam x => (x, g m) :: map (\lam s => (f s., g s.)) l'') f.func-+) idp

    \lemma toClosure {M : \Set} {R : AddMonoid} {l l' : Array (\Sigma R M)} (c : inMS l = inMS l') : Closure (~) l l'
      => Quotient.equalityClosure (\new Equivalence (Array (\Sigma R M)) (Closure (~)) {
        | ~-transitive => ctrans
        | ~-reflexive => cin (~-perm eperm-refl)
        | ~-symmetric => Closure.isSymmetric \lam p => later (~-sym p)
      }) cin $ path (\lam i => c i)

    \lemma fromClosure {M : \Set} {R : AddMonoid} {l l' : Array (\Sigma R M)} (c : Closure (~) l l') : inMS l = inMS l' \elim c
      | cin r => ~-msequiv r
      | ctrans c1 c2 => fromClosure c1 *> fromClosure c2

    \lemma unique-sum {M : \Set} {R : AddMonoid} (m : M) {l : Array (\Sigma R M)} (c : \Pi (j : Fin l.len) -> (l j). = m)
      : Closure (~) l ((R.BigSum (map __. l), m) :: nil) \elim l
      | nil => cin $ ~-sym (~-zro idp)
      | s :: l => transportInv (\lam x => Closure (~) ((s.,x) :: l) _) (c ) (~_++-right {M} {R} {(s.,m) :: nil} $ unique-sum m \lam j => c $ suc j) `ctrans` cin (~-sym (mkcon ~-+ {nil} m idp idp))
  }

\open MonoidSet

\func msMonomial {M : \Set} {R : AddMonoid} (r : R) (m : M) : MonoidSet M R
  => inMS ((r,m) :: nil)

\lemma monoidSet-ext {M : \Set} {R : AddMonoid} {x y : Quotient {Array (\Sigma R M)} (~)} (p : x = y) : x = {MonoidSet M R} y
  => path (\lam i => p i)

\func monoidSet-coefs {M : \Set} {R : AbMonoid} {P : M -> \Prop} (d : \Pi (m : M) -> Dec (P m)) (x : MonoidSet M R) : R \elim x
  | in~ l => R.BigSum $ map __. $ keep (\lam s => d s.) l
  | ~-equiv l l' r => monoidSet-coefs-coh r
  \where {
    \lemma monoidSet-coefs-coh {l l' : Array (\Sigma R M)} (e : l ~ l')
      : R.BigSum (map __. $ keep (\lam s => d s.) l) = R.BigSum (map __. $ keep (\lam s => d s.) l') \elim e
      | ~-perm e => R.BigSum_EPerm $ EPerm_map __. (EPerm_keep e)
      | ~-sym e => inv (monoidSet-coefs-coh e)
      | ~-zro {m} idp => cases (d m) \with {
        | yes e => zro-left
        | no q => idp
      }
      | ~-+ m idp idp => cases (d m) \with {
        | yes e => +-assoc
        | no q => idp
      }
  }

\func msCoef {M : DecSet} {R : AbMonoid} (p : MonoidSet M R) (m : M) : R
  => monoidSet-coefs (decideEq m) p

\lemma msCoef_monomial {M : DecSet} {R : AbMonoid} {r : R} {m : M} : msCoef (msMonomial r m) m = r
  => unfold msCoef $ rewrite (decideEq=_reduce idp) zro-right

\lemma msCoef_map {M N : DecSet} {f : M -> N} (inj : isInj f) {R E : AbMonoid} {g : AddMonoidHom R E} {p : MonoidSet M R} {m : M} : msCoef (monoidSet-map f g p) (f m) = g (msCoef p m) \elim p
  | in~ l => pmap E.BigSum (keep-lem inj g) *> inv g.func-BigSum
  \where {
    \private \lemma keep-lem {A D : \Set} {B C : DecSet} {f : B -> C} (inj : isInj f) (g : A -> D) {l : Array (\Sigma A B)} {b : B}
      : map __. (keep (\lam s => decideEq (f b) s.) (map (\lam s => (g s., f s.)) l)) = {Array D} \lam j => g (keep (\lam s => decideEq b s.) l j). \elim l
      | nil => idp
      | s :: l => cases (decideEq b s.) \with {
        | yes e => rewrite (decideEq=_reduce $ pmap f e) $ pmap (g s. ::) (keep-lem inj g)
        | no q => rewrite (decideEq/=_reduce \lam p => q (inj p)) (keep-lem inj g)
      }
  }

\instance MonoidAbMonoid (M : \Set) (R : AddMonoid) : AbMonoid (MonoidSet M R)
  | zro => in~ nil
  | + (x y : MonoidSet M R) : MonoidSet M R \with {
    | in~ l, in~ l' => in~ (l ++ l')
    | in~ l, ~-equiv l1 l2 r => monoidSet-ext $ ~-pequiv (~-perm eperm-++-comm) *> ~-pequiv (~_++-left r) *> ~-pequiv (~-perm eperm-++-comm)
    | ~-equiv l1 l2 r, in~ l' => monoidSet-ext $ ~-pequiv (~_++-left r)
  }
  | zro-left {x : MonoidSet M R} : in~ nil + x = x \elim x {
    | in~ l => idp
  }
  | +-assoc {x y z : MonoidSet M R} : (x + y) + z = x + (y + z) \elim x, y, z {
    | in~ l1, in~ l2, in~ l3 => monoidSet-ext $ pmap in~ ++-assoc
  }
  | +-comm {x y : MonoidSet M R} : x + y = y + x \elim x, y {
    | in~ l, in~ l' => monoidSet-ext $ ~-pequiv (~-perm eperm-++-comm)
  }
  \where \open MonoidSet

\instance MonoidAbGroup (M : \Set) (R : AddGroup) : AbGroup
  | AbMonoid => MonoidAbMonoid M R
  | negative (x : MonoidSet M R) : MonoidSet M R \with {
    | in~ l => in~ (map func l)
    | ~-equiv l l' r => monoidSet-ext $ Closure.toEquality inMS~ ~-pequiv (~_negative (cin r))
  }
  | negative-left {x : MonoidSet M R} : negative x + x =  \elim x {
    | in~ l => monoidSet-ext $ ~_negative-left l
  }
  \where {
    \open Transitive(Closure,cin,ctrans)

    \func func {M : \Set} {R : AddGroup} (s : \Sigma R M) => (R.negative s., s.)

    \func ~_negative {M : \Set} {R : AddGroup} {l l' : Array (\Sigma R M)} (p : Closure (~) l l')
      : Closure (~) (map func l) (map func l') \elim p
      | cin (~-perm e) => cin $ ~-perm (EPerm_map func e)
      | cin (~-sym p) => Closure.isSymmetric (\lam r => ~-sym r) $ ~_negative (cin p)
      | cin (~-zro {m} idp) => cin $ ~-zro $ pmap (\lam x => (x, m) :: map func l') R.negative_zro
      | cin (~-+ {l''} m idp idp) => ctrans (cin (~-+ m (pmap (\lam x => (x,m) :: map func l'') R.negative_+) idp)) $ cin $ ~-perm (eperm-swap idp idp idp)
      | ctrans r1 r2 => ctrans (~_negative r1) (~_negative r2)

    \func ~_negative-left {M : \Set} {R : AddGroup} (l : Array (\Sigma R M)) : inMS~ (map func l ++ l) = inMS~ nil \elim l
      | nil => idp
      | a :: l => ~-pequiv (~-perm $ EPerm_++-swap {_} {map func (a :: l)}) *> ~-pequiv (~-sym $ ~-+ a. (cong $ inv negative-right) idp) *> ~-pequiv (~-zro idp) *> ~_negative-left l
  }

\instance MonoidSemiring (M : Monoid) (R : Semiring) : Semiring
  | AbMonoid => MonoidAbMonoid M R
  | ide => in~ ((,) :: nil)
  | * (x y : MonoidSet M R) : MonoidSet M R \elim x, y {
    | in~ l, in~ l' => in~ (pairs func l l')
    | in~ l, ~-equiv l1 l2 r => monoidSet-ext $ Closure.toEquality inMS~ ~-pequiv (*-coh-right r)
    | ~-equiv l1 l2 r, in~ l => monoidSet-ext $ ~-pequiv (~-perm pairs-flip) *> Closure.toEquality inMS~ ~-pequiv (*-coh-right {M.op} {R.op} r) *> ~-pequiv (~-perm pairs-flip)
  }
  | ide-left {x} => \case \elim x \with {
    | in~ l => monoidSet-ext ide-left-aux
  }
  | ide-right {x} => \case \elim x \with {
    | in~ l => monoidSet-ext $ ~-pequiv (~-perm pairs-flip) *> ide-left-aux {M.op} {R.op}
  }
  | *-assoc {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | in~ l1, in~ l2, in~ l3 => monoidSet-ext $ ~-pequiv $ ~-perm $ eperm-= $ pairs-assoc \lam {a} {b} {c} => ext (R.*-assoc,*-assoc)
  }
  | ldistr {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | in~ l1, in~ l2, in~ l3 => monoidSet-ext $ ~-pequiv (~-perm pairs_++-right)
  }
  | rdistr {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | in~ l1, in~ l2, in~ l3 => monoidSet-ext (pmap inMS~ pairs_++-left)
  }
  | zro_*-left {x} => \case \elim x \with {
    | in~ l => idp
  }
  | zro_*-right {x} => \case \elim x \with {
    | in~ l => monoidSet-ext (pmap inMS~ pairs_nil)
  }
  \where {
    \open pairs

    \func func {M : Monoid} {R : Semiring} (s t : \Sigma R M) => (s. R.* t., s. M.* t.)

    \lemma ide-left-aux {M : Monoid} {R : Semiring} {l : Array (\Sigma R M)} : inMS~ (map (func (,)) l ++ nil) = inMS~ l
      => ~-pequiv $ ~-perm $ eperm-= $ ++_nil *> exts (\lam j => ext (R.ide-left,ide-left))

    \func *-coh-right {M : Monoid} {R : Semiring} {l l1 l2 : Array (\Sigma R M)} (r : l1 ~ l2) : Closure (~) (pairs func l l1) (pairs func l l2) \elim l
      | nil => cin (~-perm eperm-refl)
      | a :: l => ~_++ (cin $ ~_map (\new AddMonoidHom R R (a. R.*) zro_*-right ldistr) (a. M.*) r) (*-coh-right r)
  }

\instance MonoidRing (M : Monoid) (R : Ring) : Ring
  | Semiring => MonoidSemiring M R
  | AbGroup => MonoidAbGroup M R

\instance MonoidCSemiring (M : CMonoid) (R : CSemiring) : CSemiring
  | Semiring => MonoidSemiring M R
  | *-comm {x} {y} => \case \elim x, \elim y \with {
    | in~ l, in~ l' => monoidSet-ext $ ~-pequiv (~-perm pairs.pairs-flip) *> cong (ext \lam t s => ext (*-comm,*-comm))
  }

\func monoidRingHom {M : Monoid} {R : Ring} : RingHom R (MonoidRing M R) \cowith
  | func a => inMS~ ((a,M.ide) :: nil)
  | func-+ => monoidSet-ext $ ~-pequiv $ mkcon ~-+ {nil} M.ide idp idp
  | func-ide => idp
  | func-* => rewriteI {} M.ide-left idp

\instance MonoidAlgebra (M : CMonoid) (R : CRing) : CAlgebra R
  => homAlgebra {R} {\new CRing { | Ring => MonoidRing M R | *-comm => *-comm }} monoidRingHom

\func monoidSet-map {M N : \Set} (f : M -> N) (g : AddMonoidHom) (x : MonoidSet M g.Dom) : MonoidSet N g.Cod \elim x
  | in~ l => inMS~ $ map (\lam s => (g s., f s.)) l
  | ~-equiv l l' r => monoidSet-ext $ ~-pequiv (~_map g f r)

\func monoidSet-hom {M N : \Set} (f : M -> N) (g : AddMonoidHom) : AddMonoidHom (MonoidAbMonoid M g.Dom) (MonoidAbMonoid N g.Cod) (monoidSet-map f g) \cowith
  | func-zro => idp
  | func-+ {x} {y} => \case \elim x, \elim y \with {
    | in~ l, in~ l' => pmap inMS $ map_++ (\lam s => (g s., f s.))
  }

\func monoidSet-semiringHom (f : MonoidHom) (g : SemiringHom) : SemiringHom (MonoidSemiring f.Dom g.Dom) (MonoidSemiring f.Cod g.Cod) \cowith
  | AddMonoidHom => monoidSet-hom f g
  | func-ide => pmap2 (\lam x y => inMS ((x,y) :: nil)) g.func-ide f.func-ide
  | func-* {x} {y} => \case \elim x, \elim y \with {
    | in~ l, in~ l' => pmap inMS $ pairs.pairs_map (\lam s => (g s., f s.)) \lam {a} {b} => ext (g.func-*,f.func-*)
  }

\func monoidSet-ringHom (f : MonoidHom) (g : RingHom) : RingHom (MonoidRing f.Dom g.Dom) (MonoidRing f.Cod g.Cod) \cowith
  | SemiringHom => monoidSet-semiringHom f g

\lemma msMonomial_+ {M : \Set} {R : AddMonoid} {a b : R} {m : M} : msMonomial (a + b) m = msMonomial a m + msMonomial b m
  => monoidSet-ext $ ~-pequiv $ mkcon ~-+ {nil} m idp idp

\lemma msMonomial_BigSum {M : \Set} {R : AddMonoid} {l : Array R} {m : M} : msMonomial (R.BigSum l) m = BigSum (map (msMonomial __ m) l) \elim l
  | nil => msMonomial_0
  | a :: l => msMonomial_+ *> pmap (_ +) msMonomial_BigSum

\lemma msMonomial_0 {M : \Set} {R : AddMonoid} {m : M} : msMonomial R.zro m = 
  => monoidSet-ext $ ~-pequiv $ MonoidSet.~-zro idp

\lemma msMonomial_* {M : Monoid} {R : Semiring} {a b : R} : msMonomial (a * b) M.ide = msMonomial a M.ide * msMonomial b M.ide
  => monoidSet-ext $ unfold MonoidSemiring.func $ rewrite ide-left idp

\lemma msMonomial_pow {M : Monoid} {R : Semiring} {r : R} {m : M} {n : Nat} : Monoid.pow (msMonomial r m) n = msMonomial (Monoid.pow r n) (Monoid.pow m n) \elim n
  |  => idp
  | suc n => rewrite msMonomial_pow idp

\lemma msMonomial-split {M : Monoid} {R : Semiring} {a : R} {m : M} : msMonomial a M.ide * msMonomial R.ide m = msMonomial a m
  => pmap2 (\lam x y => inMS ((x,y) :: nil)) ide-right ide-left

\lemma msMonomial_BigSum-split {M : \Set} {R : AddMonoid} {l : Array (\Sigma R M)} : BigSum (map (\lam s => msMonomial s. s.) l) = inMS l \elim l
  | nil => idp
  | s :: l => pmap (_ +) msMonomial_BigSum-split

\lemma msMonomial_BigProd {M : Monoid} {R : Semiring} (l : Array (\Sigma R M))
  : Monoid.BigProd (map (\lam s => msMonomial s. s.) l) = msMonomial (Monoid.BigProd $ map __. l) (Monoid.BigProd $ map __. l) \elim l
  | nil => idp
  | s :: l => pmap (_ *) (msMonomial_BigProd l)

\lemma msMonomial_BigProd_ide {M : Monoid} {R : Semiring} {l : Array M}
  : Monoid.BigProd (map (\lam m => msMonomial R.ide m) l) = msMonomial R.ide (Monoid.BigProd l)
  => msMonomial_BigProd (map (\lam m => (R.ide,m)) l) *> pmap (msMonomial __ _) Monoid.BigProd_replicate1

\lemma monoidSet-coefs_+ {M : \Set} {R : AbMonoid} {P : M -> \Prop} {d : \Pi (m : M) -> Dec (P m)} {x y : MonoidSet M R}
  : monoidSet-coefs d (x + y) = monoidSet-coefs d x + monoidSet-coefs d y \elim x, y
  | in~ l, in~ l' => pmap R.BigSum (pmap (map __.) keep_++ *> map_++ __.) *> R.BigSum_++

\lemma monoidSet-coefs_BigSum {M : \Set} {R : AbMonoid} {P : M -> \Prop} {d : \Pi (m : M) -> Dec (P m)} {l : Array (MonoidSet M R)}
  : monoidSet-coefs d (BigSum l) = BigSum (map (monoidSet-coefs d) l) \elim l
  | nil => idp
  | a :: l => monoidSet-coefs_+ *> pmap (_ +) monoidSet-coefs_BigSum

\lemma msCoef-split {M : DecSet} {R : AbMonoid} (p : MonoidSet M R)
  : ∃ (l : Array M) (\Pi {i j : Fin l.len} -> l i = l j -> i = j) (p = BigSum (map (\lam m => msMonomial (msCoef p m) m) l)) \elim p
  | in~ l => inP (nub (map __. l), nub-isInj, inv msMonomial_BigSum-split *> AbMonoid.BigSum_EPerm (EPerm_map (\lam s => msMonomial s. s.) nub-split) *>
      pmap BigSum (inv (Big++_map (\lam s => msMonomial s. s.))) *> BigSum_Big++ *>
      (pmap (\lam x => BigSum (map x _)) {\lam m => BigSum (map (\lam s => msMonomial s. s.) (keep (\lam s => M.decideEq m s.) l))}
          (ext \lam m => msMonomial_BigSum-split *> fromClosure (unique-sum m \lam j => inv $ keep.satisfies {\Sigma R M} (\lam s => decideEq m s.))) : BigSum (map _ (nub (map __. l))) = _))

\lemma msCoefs-fin {M : DecSet} {R : AbMonoid} {Rd : DecSet R} (p : MonoidSet M R) : FinSet (\Sigma (m : M) (msCoef p m /= ))
  => \case msCoef-split p \with {
       | inP (l, inj, q) =>
        \let l' : Array M => remove (\lam m => decideEq (msCoef p m) ) l
        \in KFinSet.KFin+Dec=>Fin (\new KFinSet {
         | finCard => l'.len
         | finSurj => inP (\lam j => (l' j, remove.no-element \lam m => decideEq (msCoef p m) ), \lam x => \case index-dec l' x. \with {
           | inl s => inP (s., ext s.)
           | inr r => absurd $ x. $ rewrite q $ monoidSet-coefs_BigSum *> BigSum_zro \lam j => BigSum_zro $ later $ rewrite (decideEq/=_reduce \lam p' => r $ rewrite p' $ remove.element $ later $ rewriteI p' x.) \case __
         })
       }) {SubDecSet}
     }

\lemma msCoef/=0 {M : DecSet} {R : AbMonoid} {Rd : DecSet R} {p : MonoidSet M R} (p/=0 : p /= ) : ∃ (m : M) (msCoef p m /= )
  => \case KFinSet.dec {msCoefs-fin p} \with {
       | yes e => e
       | no q => absurd $ p/=0 \case msCoef-split p \with {
         | inP (l,_,r) => r *> BigSum_zro \lam j => pmap (msMonomial __ _) (separatedEq \lam s => q $ inP $ later (l j, s)) *> msMonomial_0
       }
  }

\func msCoef/=0_Index {M : DecSet} {R : AbMonoid} {l : Array (\Sigma R M)} {m : M} (p : msCoef (inMS l) m /= ) : Index m (map __. l)
  => \case index-dec (map __. l) m \with {
    | inl r => r
    | inr q => absurd $ p $ pmap (\lam (l : Array (\Sigma R M)) => BigSum $ map __. l) $ keep-none \lam j p => q (j, inv p)
  }

\type DecMonoidSet (M : \Set) (R : AddPointed)
  => Quotient {Type M R} \lam s t => EPerm s. t.
  \where {
    \func Type  (M : \Set) (R : AddPointed) => \Sigma (l : Array (\Sigma R M)) (\Pi {i j : Fin l.len} -> (l i). = (l j). -> i = j) (\Pi (j : Fin l.len) -> (l j). /= )

    \func inDMS {M : \Set} {R : AddPointed} (s : Type M R) : DecMonoidSet M R => in~ s

    \lemma ~-dmsequiv {M : \Set} {R : AddPointed} {s t : Type M R} (p : EPerm s. t.) : inDMS s = inDMS t
      => path \lam i => ~-pequiv p i

    \lemma unext {M : \Set} {R : AddPointed} {s t : Type M R} (p : inDMS s = inDMS t) : TruncP (EPerm s. t.)
      => Quotient.equalityClosure (Equivalence.map __. EPerm.EPerm-equivalence) (\lam e => inP e) (path \lam i => p i)
  }

\func decToMonoidSet {M : \Set} {R : AddMonoid} (p : DecMonoidSet M R) : MonoidSet M R \elim p
  | in~ s => in~ s.
  | ~-equiv x y r => ~-msequiv (~-perm r)

\lemma monoidSetDec-equiv {M : DecSet} {R : AbMonoid} {Rd : DecSet R} : Equiv (decToMonoidSet {M} {R})
  => Equiv.fromInjSurj _ (\lam {in~ s} {in~ t} q => \case Transitive.Closure.univ (Equivalence.map msNorm $ EPerm-equivalence) (\lam e => inP (msNorm_~ e)) (MonoidSet.toClosure q) \with {
       | inP r => DecMonoidSet.~-dmsequiv $ transport2 EPerm (msNorm=msNorm' *> msNorm'-norm) (msNorm=msNorm' *> msNorm'-norm) r
     }) \lam (in~ l) => inP (DecMonoidSet.inDMS (msNorm l, remove.no-repeats nub-isInj, \lam j => remove.no-element (\lam m => decideEq (msCoef (inMS l) m) )),
                             inv $ rewrite msNorm=msNorm' $ ~-msequiv (~-perm nub-split) *> fromClosure +_~ *> fromClosure remove_~)
  \where \private {
    \func msNormVars {Rd : DecSet R} (p : MonoidSet M R) (l : Array (\Sigma R M)) => remove (\lam m => decideEq (msCoef p m) ) $ nub (map __. l)

    \func msNorm {Rd : DecSet R} (l : Array (\Sigma R M)) => map (\lam m => (msCoef (inMS l) m, m)) (msNormVars (inMS l) l)

    \func msNorm' {Rd : DecSet R} (l : Array (\Sigma R M)) => remove (\lam s => decideEq s. ) $ map (\lam m => (msCoef (inMS l) m, m)) $ nub (map __. l)

    \lemma +_~ {Rd : DecSet R} {lm : Array M} {lp : Array (\Sigma R M)} : Closure (~) (Big (++) nil (map (\lam m => keep (\lam s => decideEq m s.) lp) lm)) (map (\lam m => (msCoef (inMS lp) m, m)) lm)
      => transportInv (Closure (~) _) Big++-split $ later $ ~_Big++ {_} {_} {_} {map (\lam m => keep (\lam s => decideEq m s.) lp) lm} {map (\lam m => (msCoef (inMS lp) m, m) :: nil) lm} \lam j => unique-sum (lm j) \lam k => inv $ keep.satisfies (\lam s => decideEq (lm j) s.) {lp}

    \func remove_~ {Rd : DecSet R} {l : Array (\Sigma R M)} : Closure (~) l (remove (\lam s => decideEq s. ) l) \elim l
      | nil => cin (~-perm eperm-refl)
      | a :: l => mcases \with {
        | yes p => ctrans (cin $ ~-zro $ pmap (\lam x => (x,a.) :: l) p) remove_~
        | no q => ~_++-right {_} {_} {a :: nil} remove_~
      }

    \lemma msNorm=msNorm' {Rd : DecSet R} {l : Array (\Sigma R M)} : msNorm l = msNorm' l
      => inv (remove_map (\lam m => (msCoef (inMS l) m, m)))

    \lemma msNorm'-norm {Rd : DecSet R} {s : DecMonoidSet.Type M R} : msNorm' s. = s.
      => pmap (\lam x => remove _ (map (\lam m => (msCoef (inMS s.) m, m)) x)) (nub_id $ later s.) *> pmap (remove _) (exts \lam j => pmap (__, (s. j).) $
          pmap {Array (\Sigma R M)} (\lam x => BigSum $ map __. x) (keep-unique idp \lam i q => s. (inv q)) *> zro-right) *> remove-none s.

    \lemma msNormVars-norm {Rd : DecSet R} {p : MonoidSet M R} {l : Array M} (inj : isInj l) (s : \Pi (j : Fin l.len) -> msCoef p (l j) /= ) : msNormVars p (map (\lam m => (msCoef p m, m)) l) = l
      => pmap (remove _) (nub_id inj) *> remove-none s

    \func msNorm_~ {Rd : DecSet R} {l l' : Array (\Sigma R M)} (e : l ~ l') : EPerm (msNorm l) (msNorm l')
      => transport (\lam x => EPerm _ (map x _)) {\lam m => (msCoef (inMS l) m, m)} (ext \lam m => pmap (\lam x => (msCoef x m, m)) (~-msequiv e)) (EPerm.EPerm_map (\lam m => (msCoef (inMS l) m, m)) (msNormVars_~' e))

    \func msNormVars_~' {Rd : DecSet R} {l l' : Array (\Sigma R M)} (e : l ~ l') : EPerm (msNormVars (inMS l) l) (msNormVars (inMS l') l')
      => transport (EPerm _) (pmap (msNormVars __ l') (~-msequiv e)) (msNormVars_~ e idp)

    \func msNormVars_~ {Rd : DecSet R} {p : MonoidSet M R} {l l' : Array (\Sigma R M)} (e : l ~ l') (pp : p = inMS l) : EPerm (msNormVars p l) (msNormVars p l') \elim e
      | ~-perm e => EPerm_remove $ EPerm_nub $ EPerm_map __. e
      | ~-sym e => eperm-sym $ msNormVars_~ e $ pp *> ~-msequiv (~-sym e)
      | ~-zro {m} idp => unfold msNormVars $ mcases {} \with {
        | yes e => eperm-= $ remove_remove *> remove.equals (\lam {a} => ||.rec' (\lam x => x) \lam p => later $ rewriteI p e) (\lam {a} => byLeft)
        | no q => rewrite remove-swap \have | i1 => msCoef/=0_Index (rewrite (pp *> ~-msequiv (~-zro idp)) in q)
                                            | i2 => nub-isSurj (map __. l') i1.
                                            | i : Index m (msNormVars p l') => transport (Index __ _) (i2. *> i1.) $ remove.element \lam r => q $ inv (pmap (msCoef p) $ i2. *> i1.) *> r
                                      \in rewriteI i. $ eperm-sym $ eperm-remove (remove.no-repeats nub-isInj) i.
      }
      | ~-+ m q1 q2 => EPerm_remove $ later $ rewrite (q1, q2) $ eperm-= $ pmap (m ::) $ later $ rewrite (decideEq=_reduce idp) $ remove.equals (\lam {a} => byLeft) (\lam {a} => ||.rec' (\lam x => x) (\lam x => x)) *> inv remove_remove
  }

\func evalMS {M : \Set} {R : Semiring} (x : MonoidSet M R) (f : M -> R) : R \elim x
  | in~ l => R.BigSum $ map (\lam s => s. * f s.) l
  | ~-equiv l l' r => evalMS-coh f r
  \where {
    \lemma evalMS-coh {M : \Set} {R : Semiring} (f : M -> R) {l l' : Array (\Sigma R M)} (r : l ~ l')
      : R.BigSum (map (\lam s => s. * f s.) l) = R.BigSum (map (\lam s => s. * f s.) l') \elim r
      | ~-perm e => R.BigSum_EPerm $ EPerm_map (\lam s => s. * f s.) e
      | ~-sym r => inv (evalMS-coh f r)
      | ~-zro idp => pmap (`+ _) zro_*-left *> zro-left
      | ~-+ m idp idp => pmap (`+ _) rdistr *> +-assoc
  }

\func evalMSMonoidHom {M : \Set} {R : Semiring} (f : M -> R) : AddMonoidHom (MonoidAbMonoid M R) R \cowith
  | func => evalMS __ f
  | func-zro => idp
  | func-+ {x} {y} => \case \elim x, \elim y \with {
    | in~ l, in~ l' => pmap R.BigSum (map_++ (\lam s => s. * f s.)) *> R.BigSum_++
  }

\func evalMSSemiringHom {M : Monoid} {R : CSemiring} (f : MonoidHom M R) : SemiringHom (MonoidSemiring M R) R \cowith
  | AddMonoidHom => evalMSMonoidHom f
  | func-ide => simplify f.func-ide
  | func-* {x} {y} => \case \elim x, \elim y \with {
    | in~ l, in~ l' => pairs.pairs-distr (\lam s => s. * f s.) \lam {a} {b} => unfold MonoidSemiring.func (rewrite f.func-* equation)
  }

\func evalMSRingHom {M : Monoid} {R : CRing} (f : MonoidHom M R) : RingHom (MonoidRing M R) R \cowith
  | SemiringHom => evalMSSemiringHom f

\lemma evalMS_monomial {M : AddPointed} {R : Semiring} {f : PointedHom M R} {a : R} : evalMS (msMonomial a M.zro) f = a
  => zro-right *> pmap (a *) func-ide *> ide-right

\lemma evalMS_map {M N : Monoid} {R : CRing} {f : M -> N} {x : MonoidSet M R} {g : N -> R}
  : evalMS (monoidSet-map f (id R) x) g = evalMS x (\lam m => g (f m)) \elim x
  | in~ l => idp

\lemma evalMS_map2 {M : \Set} {R S : Semiring} {x : MonoidSet M R} {f : M -> R} (g : SemiringHom R S)
  : evalMS (monoidSet-map (\lam y => y) g x) (\lam m => g (f m)) = g (evalMS x f) \elim x
  | in~ l => inv $ g.func-BigSum *> pmap BigSum (exts \lam j => g.func-*)

\func polyToMonoidSet {M : Monoid} {R : Semiring} (m : M) (p : Poly R) : MonoidSet M R \elim p
  | pzero => 
  | padd p a => polyToMonoidSet m p * msMonomial  m + msMonomial a ide
  | peq i => ~-pequiv {_} {_} {(R.zro,M.ide) :: nil} {nil} (MonoidSet.~-zro idp) i

\func polyToMonoidSetHom {M : Monoid} {R : Ring} (m : M) : AddMonoidHom (PolyRing R) (MonoidRing M R) \cowith
  | func => polyToMonoidSet m
  | func-zro => idp
  | func-+ {p q : Poly R} : polyToMonoidSet m (p + q) = polyToMonoidSet m p + polyToMonoidSet m q \elim p, q {
    | pzero, q => inv zro-left
    | p, pzero => pmap (polyToMonoidSet m) +-comm *> inv zro-right
    | padd p a, padd q b => rewrite (func-+,rdistr,msMonomial_+) $ +-assoc *> pmap (_ +) (later (inv +-assoc) *> pmap (`+ _) +-comm *> +-assoc) *> inv +-assoc
  }

\func polyToMonoidSetRingHom {M : CMonoid} {R : CRing} (m : M) : RingHom (PolyRing R) (MonoidRing M R) \cowith
  | AddMonoidHom => polyToMonoidSetHom m
  | func-ide => idp
  | func-* {p q : Poly R} : polyToMonoidSet m (p * q) = polyToMonoidSet m p * polyToMonoidSet m q \elim p {
    | pzero => inv zro_*-left
    | padd p a => polyToMonoidSetHom.func-+ *> pmap2 (+) (pmap (_ +) msMonomial_0 *> zro-right *> pmap (`* _) func-* *> *-assoc *> pmap (_ *) *-comm *> inv *-assoc) func-*c *> inv rdistr
  }
  \where {
    \lemma func-*c {m : M} {a : R} {p : Poly R} : polyToMonoidSet m (a PolyRing.*c p) = msMonomial a ide * polyToMonoidSet m p \elim p
      | pzero => idp
      | padd p b => pmap (__ * _ + _) func-*c *> pmap2 (+) *-assoc simplify *> inv ldistr
  }

\lemma polyToMonoidSet-eval {R : CRing} {M : Monoid} {p : Poly R} {f : MonoidHom M R} {m : M} : evalMS (polyToMonoidSet m p) f = polyEval p (f m) \elim p
  | pzero => idp
  | padd p a => func-+ {evalMSRingHom f} *> pmap2 (+) (func-* *> pmap2 (*) polyToMonoidSet-eval simplify) (unfold $ rewrite f.func-ide simplify)

\lemma monoidRingHom-unique {M : Monoid} {R S : CRing} {f g : RingHom (MonoidRing M R) S} (p : \Pi (r : R) -> f (msMonomial r ide) = g (msMonomial r ide)) (q : \Pi (m : M) -> f (msMonomial  m) = g (msMonomial  m)) (x : MonoidSet M R) : f x = g x \elim x
  | in~ l => pmap f monoidSet-list *> f.func-BigSum *> pmap BigSum (exts \lam j => simplify *> f.func-* *> pmap2 (*) (p (l j).) (q (l j).) *> inv g.func-* *> simplify) *> inv g.func-BigSum *> inv (pmap g monoidSet-list)
  \where {
    \lemma monoidSet-list {M : \Set} {R : AddMonoid} {l : Array (\Sigma R M)} : inMS l = BigSum \lam j => msMonomial (l j). (l j). \elim l
      | nil => idp
      | a :: l => pmap (_ +) monoidSet-list
  }