\import Algebra.Monoid
\import Algebra.Pointed.PointedHom
\import Logic
\import Paths
\import Paths.Meta
\import Set.Fin

\record MonoidHom \extends PointedHom {
  \override Dom : Monoid
  \override Cod : Monoid
  | func-* {x y : Dom} : func (x * y) = func x * func y

  \lemma func-pow {x : Dom} {n : Nat} : func (Monoid.pow x n) = Monoid.pow (func x) n \elim n
    |  => func-ide
    | suc n => func-* *> pmap (`* _) func-pow

  \lemma func-BigProd {l : Array Dom} : func (Monoid.BigProd l) = Monoid.BigProd (\lam j => func (l j)) \elim l
    | nil => func-ide
    | a :: l => func-* *> pmap (_ *) func-BigProd

  \lemma func-LDiv {a b : Dom} (d : Monoid.LDiv a b) : Monoid.LDiv (func a) (func b) (func d.inv) \cowith
    | inv-right => inv func-* *> pmap func d.inv-right

  \lemma func-Inv {a : Dom} (d : Monoid.Inv a) : Monoid.Inv (func a) (func d.inv) \cowith
    | inv-left => inv func-* *> pmap func d.inv-left *> func-ide
    | inv-right => inv func-* *> pmap func d.inv-right *> func-ide
} \where {
  \func equals {M N : Monoid} {f g : MonoidHom M N} (p : \Pi (x : M) -> f x = g x) : f = g
    => exts p

  \func id {M : Monoid} : MonoidHom M M \cowith
    | func x => x
    | func-ide => idp
    | func-* => idp

  \open Monoid(Inv)

  \func presInv (h : MonoidHom) (e : Inv {h.Dom}) : Inv (h e) \cowith
    | inv => h e.inv
    | inv-left => inv h.func-* *> pmap h e.inv-left *> h.func-ide
    | inv-right => inv h.func-* *> pmap h e.inv-right *> h.func-ide

  \lemma presInvElem (h : MonoidHom) (e : Inv {h.Dom}) (e' : Inv (h e)) : h e.inv = e'.inv
    => pmap (\lam (j : Inv) => j.inv) (Inv.levelProp (\new Inv (h e) {
      | inv => h e.inv
      | inv-left => inv h.func-* *> pmap h e.inv-left *> h.func-ide
      | inv-right => inv h.func-* *> pmap h e.inv-right *> h.func-ide
    }) e')
}

\record AddMonoidHom \extends AddPointedHom {
  \override Dom : AddMonoid
  \override Cod : AddMonoid
  | func-+ {x y : Dom} : func (x + y) = func x + func y

  \lemma func-BigSum {l : Array Dom} : func (AddMonoid.BigSum l) = AddMonoid.BigSum (\lam j => func (l j)) \elim l
    | nil => func-zro
    | a :: l => func-+ *> pmap (_ +) func-BigSum

  \lemma func-*n {n : Nat} {x : Dom} : func (n AddMonoid.*n x) = n AddMonoid.*n func x \elim n
    |  => func-zro
    | suc n => func-+ *> pmap (`+ _) func-*n
} \where {
  \use \coerce toMonoidHom (f : AddMonoidHom) : MonoidHom \cowith
    | Dom => f.Dom
    | Cod => f.Cod
    | func => f
    | func-* => func-+
    | func-ide => func-zro

  \func id {M : AddMonoid} : AddMonoidHom M M \cowith
    | func x => x
    | func-zro => idp
    | func-+ => idp

  \lemma func-FinSum {A B : AbMonoid} (f : AddMonoidHom A B) {J : FinSet} {a : J -> A} : f (A.FinSum a) = B.FinSum (\lam j => f (a j))
    => \case A.FinSum_char a \with {
         | inP (e,q) => pmap f q *> f.func-BigSum *> inv (B.FinSum_char2 e)
       }
}