\import Algebra.Group
\import Algebra.Group.GroupHom
\import Algebra.Group.SubGroup
\import Algebra.Meta
\import Algebra.Monoid
\import Function
\import Function.Meta
\import Meta
\import Paths
\import Relation.Equivalence

\func \infix  // (G : Group) (H : NormalSubGroup G) : Group
  => H.Quot

\func kerQuotHom {G H : Group} (f : GroupHom G H) : GroupHom (G // KernelGroup f) H \cowith
  | func (x : G // KernelGroup f) : H \with {
    | in~ n => f n
    | ~-equiv y x r => (H.makeInv (inverse (f y))).inv-cancel-left $ inverse-left *> inv r *> f.func-* *> pmap (* _) f.func-inverse
  }
  | func-* {in~ x} {in~ y} => f.func-*

\lemma FirstIsoTheorem {G H : Group} (f : GroupHom G H) (p : IsSurj f) : (kerQuotHom f).IsIsomorphism
  => (Kernel-trivial-char. $ later \lam {in~ a} q => inv $ ~-pequiv $ pmap f equation.group *> q,
      IsSurj.factor {G} {_} {H} {NormalSubGroup.quotHom} p)