\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Pointed
\import Algebra.Pointed.Category
\import Category (Cat)
\import Category.Meta
\import Category.Subcat
\import Equiv
\import Function
\import Function.Meta
\import Logic
\import Paths
\import Paths.Meta
\import Set.Category
\import Set.Fin

\instance GroupCat : Cat Group
  => subCat (\new Embedding {
    | f G => G
    | isEmb G H => \new Retraction {
      | sec => Group.equals G H
      | f_sec => idpe
    }
  })

\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
} \where {
  \use \coerce toMonoidHom (f : AddMonoidHom) : MonoidHom \cowith
    | Dom => f.Dom
    | Cod => f.Cod
    | func => f
    | func-* => func-+
    | func-ide => func-zro

  \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 *> func-BigSum *> inv (B.FinSum_char2 _ e)
       }
}

\instance AddMonoidCat : Cat AddMonoid
  | Hom M N => AddMonoidHom M N
  | id => id
  | o g f => \new AddMonoidHom {
    | func x => g (f x)
    | func-zro => pmap g func-zro *> func-zro
    | func-+ => pmap g func-+ *> func-+
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam {X} {A} {B} (p1 : AddMonoidHom) p2 => exts (p1.func-zro, \lam _ _ => p1.func-+))
  \where
    \func id (M : AddMonoid) : AddMonoidHom M M \cowith
      | func x => x
      | func-zro => idp
      | func-+ => idp

\instance KerAddMonoid (f : AddMonoidHom) : AddMonoid
  | AddPointed => KerAddPointed f
  | + a b => (a. + b., func-+ *> pmap2 (+) a. b. *> zro-left)
  | zro-left => ext zro-left
  | zro-right => ext zro-right
  | +-assoc => ext +-assoc

\func KerMonoidHom (f : AddMonoidHom) : AddMonoidHom (KerAddMonoid f) f.Dom \cowith
  | AddPointedHom => KerPointedHom f
  | func-+ => idp

\instance KerAbMonoid {A : AbMonoid} (f : AddMonoidHom A) : AbMonoid (Kernel f)
  | AddMonoid => KerAddMonoid f
  | +-comm => ext +-comm

\instance ImageAddMonoid (f : AddMonoidHom) : AddMonoid
  | AddPointed => ImageAddPointed f
  | + a b => (a. + b., \case a., b. \with {
    | inP t, inP s => inP (t. + s., func-+ *> pmap2 (+) t. s.)
  })
  | zro-left => ext zro-left
  | zro-right => ext zro-right
  | +-assoc => ext +-assoc

\func ImageMonoidLeftHom (f : AddMonoidHom) : AddMonoidHom f.Dom (ImageAddMonoid f) \cowith
  | AddPointedHom => ImagePointedLeftHom f
  | func-+ => ext func-+

\func ImageMonoidRightHom (f : AddMonoidHom) : AddMonoidHom (ImageAddMonoid f) f.Cod \cowith
  | AddPointedHom => ImagePointedRightHom f
  | func-+ => idp

\instance ImageAbMonoid {A : AddMonoid} {B : AbMonoid} (f : AddMonoidHom A B) : AbMonoid
  | AddMonoid => ImageAddMonoid f
  | +-comm => ext +-comm

\record AddGroupHom \extends AddMonoidHom {
  \override Dom : AddGroup
  \override Cod : AddGroup
  | func-zro => AddGroup.cancel-left (func ) (inv func-+ *> pmap func zro-right *> inv zro-right)

  \lemma func-negative {x : Dom} : func (negative x) = negative (func x)
    => AddGroup.cancel-left (func x) (inv (negative-right *> inv (pmap func negative-right *> func-zro) *> func-+))

  \lemma injective (p : \Pi {a : Dom} -> func a =  -> a = ) : isInj func
    => \lam q => AddGroup.fromZero $ p $ func-+ *> pmap (_ +) func-negative *> AddGroup.toZero q
}

\instance AddGroupCat : Cat AddGroup
  | Hom G H => AddGroupHom G H
  | id => id
  | o g f => \new AddGroupHom {
    | func x => g (f x)
    | func-+ => pmap g func-+ *> func-+
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam {X} {A} {B} (p1 : AddGroupHom) p2 => exts (p1.func-zro, \lam _ _ => p1.func-+, AddGroup.negative-equality A B p1.func-zro p1.func-+))
  \where
    \func id (G : AddGroup) : AddGroupHom G G \cowith
      | func x => x
      | func-+ => idp

\instance AbGroupCat : Cat AbGroup
  => subCat (\new Embedding {AbGroup} {AddGroup} {
    | f A => A
    | isEmb A B => \new Retraction {
      | sec => AbGroup.equals A B
      | f_sec => idpe
    }
  })

\instance KerAddGroup (f : AddGroupHom) : AddGroup
  | AddMonoid => KerAddMonoid f
  | negative a => (negative a., f.func-negative *> pmap negative a. *> AddGroup.negative_zro)
  | negative-left => ext negative-left
  | negative-right => ext negative-right

\func KerGroupHom (f : AddGroupHom) : AddGroupHom (KerAddGroup f) f.Dom \cowith
  | AddMonoidHom => KerMonoidHom f

\instance KerAbGroup {A : AbGroup} (f : AddGroupHom A) : AbGroup
  | AddGroup => KerAddGroup f
  | AbMonoid => KerAbMonoid f

\lemma kernel=0<->inj {f : AddGroupHom} : isInj f <-> (\Pi (x : Kernel f) -> x = )
  => (\lam fi x => ext $ fi $ x. *> inv func-zro,
      \lam c {a} {a'} p => AddGroup.fromZero $ pmap __. (c (a - a', func-+ *> pmap (_ +) f.func-negative *> AddGroup.toZero p)))

\instance ImageAddGroup (f : AddGroupHom) : AddGroup
  | AddMonoid => ImageAddMonoid f
  | negative a => (negative a., TruncP.map a. \lam s => (negative s., f.func-negative *> pmap negative s.))
  | negative-left => ext negative-left
  | negative-right => ext negative-right

\func ImageGroupLeftHom (f : AddGroupHom) : AddGroupHom f.Dom (ImageAddGroup f) \cowith
  | AddMonoidHom => ImageMonoidLeftHom f

\func ImageGroupRightHom (f : AddGroupHom) : AddGroupHom (ImageAddGroup f) f.Cod \cowith
  | AddMonoidHom => ImageMonoidRightHom f

\instance ImageAbGroup {A : AddGroup} {B : AbGroup} (f : AddGroupHom A B) : AbGroup
  | AddGroup => ImageAddGroup f
  | AbMonoid => ImageAbMonoid f