Require Import Basics Types Truncations.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Cubical.DPath WildCat.
Require Import Colimits.Coeq.
Require Import Algebra.AbGroups.AbelianGroup.
Require Import Modalities.ReflectiveSubuniverse.

(** * Abelianization *)

(** In this file we define what it means for a group homomorphism [G -> H] into an abelian group [H] to be an abelianization. We then construct an example of an abelianization. *)

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.
Local Open Scope wc_iso_scope.

(** ** Definition of abelianization.

  A "unit" homomorphism [eta : G -> G_ab], with [G_ab] abelian, is considered an abelianization if and only if for all homomorphisms [G -> A], where [A] is abelian, there exists a unique [g : G_ab -> A] such that [h == g o eta X].   We express this in funext-free form by saying that precomposition with [eta] in the wild 1-category [Group] induces an equivalence of hom 0-groupoids, in the sense of WildCat/EquivGpd.

  Unfortunately, if [eta : GroupHomomorphism G G_ab] and we write [cat_precomp A eta] then Coq is unable to guess that the relevant 1-category is [Group].  Even writing [cat_precomp (A := Group) A eta] isn't good enough, I guess because the typeclass inference that finds the instance [is01cat_group] doesn't happen until after the type of [eta] would have to be resolved to a [Hom] in some wild category.  However, with the following auxiliary definition we can force the typeclass inference to happen first.  (It would be worth thinking about whether the design of the wild categories library could be improved to avoid this.)  *)
Definition group_precomp {a b} := @cat_precomp Group _ _ a b.

Class IsAbelianization {G : Group} (G_ab : AbGroup)
      (eta : GroupHomomorphism G G_ab)
  := issurjinj_isabel :: forall (A : AbGroup),
      IsSurjInj (group_precomp A eta).

Definition isequiv_group_precomp_isabelianization `{Funext}
  {G : Group} {G_ab : AbGroup} (eta : GroupHomomorphism G G_ab)
  `{!IsAbelianization G_ab eta} (A : AbGroup)
  : IsEquiv (group_precomp A eta).
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
IsEquiv (group_precomp A eta)
Proof.
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
IsEquiv (group_precomp A eta)
  snapply isequiv_adjointify.
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
(G $-> A) -> G_ab $-> A
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
group_precomp A eta o ?g == idmap
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
?g o group_precomp A eta == idmap
  -
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
(G $-> A) -> G_ab $-> A intros g.
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
g: G $-> A
G_ab $-> A
    exact (surjinj_inv (group_precomp A eta) g).
  -
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
group_precomp A eta
o (fun g : G $-> A =>
   surjinj_inv (group_precomp A eta) g) == idmap intros f.
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
f: G $-> A
group_precomp A eta
  (surjinj_inv (group_precomp A eta) f) = f
    snapply equiv_path_grouphomomorphism.
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
f: G $-> A
group_precomp A eta
  (surjinj_inv (group_precomp A eta) f) == f
    exact (eisretr0gpd_inv (group_precomp A eta) f).
  -
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
(fun g : G $-> A =>
 surjinj_inv (group_precomp A eta) g)
o group_precomp A eta == idmap intros f.
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
f: G_ab $-> A
surjinj_inv (group_precomp A eta)
  (group_precomp A eta f) = f
    snapply equiv_path_grouphomomorphism.
H: Funext
G: Group
G_ab: AbGroup
eta: GroupHomomorphism G G_ab
IsAbelianization0: IsAbelianization G_ab eta
A: AbGroup
f: G_ab $-> A
surjinj_inv (group_precomp A eta)
  (group_precomp A eta f) == f
    exact (eissect0gpd_inv (group_precomp A eta) f).
Defined.

Definition equiv_group_precomp_isabelianization `{Funext}
  {G : Group} {G_ab : AbGroup} (eta : GroupHomomorphism G G_ab)
  `{!IsAbelianization G_ab eta} (A : AbGroup)
  : (G_ab $-> A) <~> (G $-> A)
  := Build_Equiv _ _ _ (isequiv_group_precomp_isabelianization eta A).

(** Here we define abelianization as a HIT. Specifically as a set-coequalizer of the following two maps [fun '(a, b, c) => a * (b * c)] and [fun '(a, b, c) => a * (c * b)].

From this we can show that Abel G is an abelian group.

In fact this models the following HIT:

<<
HIT Abel (G : Group) := 
 | abel_in : G -> Abel G
 | abel_in_comm : forall x y z, abel_in (x * (y * z)) = abel_in (x * (z * y)).
>>

We also derive [abel_in] and [abel_in_comm] from our coequalizer definition, and even prove the induction and computation rules for this HIT.

This HIT was suggested by Dan Christensen. *)

Section Abel.

  (** Let G be a group. *)
  Context (G : Group).

  (** We locally define a map uncurry2 that lets us uncurry [A * B * C -> D] twice. *)
  Local Definition uncurry2 {A B C D : Type}
    : (A -> B -> C -> D) -> A * B * C -> D
    := fun f '(a, b, c) => f a b c.

  (** The type [Abel] is defined to be the set coequalizer of the following maps [G^3 -> G]. *)
  Definition Abel
    := Tr 0 (Coeq
      (uncurry2 (fun a b c : G => a * (b * c)))
      (uncurry2 (fun a b c : G => a * (c * b)))).

  (** We have a natural map from [G] to [Abel G]. *)
  Definition abel_in : G -> Abel := tr o coeq.

  (** This map satisfies the condition [ab_comm]. It's a form of commutativity in a right factor. *)
  Definition abel_in_comm a b c
    : abel_in (a * (b * c)) = abel_in (a * (c * b))
    := ap tr (cglue (a, b, c)).

  (** It is clear that Abel is a set. *)
  Definition istrunc_abel : IsHSet Abel := _.

  (** We can derive the induction principle from the ones for truncation and the coequalizer. *)
  Definition Abel_ind (P : Abel -> Type) `{forall x, IsHSet (P x)} 
    (a : forall x, P (abel_in x))
    (c : forall x y z, abel_in_comm x y z # a (x * (y * z)) = a (x * (z * y)))
    : forall (x : Abel), P x.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (abel_in x)
c: forall x y z : G,
transport P (abel_in_comm x y z) (a (x * (y * z))) =
a (x * (z * y))
forall x : Abel, P x
  Proof.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (abel_in x)
c: forall x y z : G,
transport P (abel_in_comm x y z) (a (x * (y * z))) =
a (x * (z * y))
forall x : Abel, P x
    rapply Trunc_ind.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (abel_in x)
c: forall x y z : G,
transport P (abel_in_comm x y z) (a (x * (y * z))) =
a (x * (z * y))
forall
a : Coeq (uncurry2 (fun a b c : G => a * (b * c)))
      (uncurry2 (fun a b c : G => a * (c * b))),
P (tr a)
    snapply Coeq_ind.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (abel_in x)
c: forall x y z : G,
transport P (abel_in_comm x y z) (a (x * (y * z))) =
a (x * (z * y))
forall a : G,
(fun
   w : Coeq
         (uncurry2 (fun a0 b c : G => a0 * (b * c)))
         (uncurry2 (fun a0 b c : G => a0 * (c * b)))
 => P (tr w)) (coeq a)
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (abel_in x)
c: forall x y z : G,
transport P (abel_in_comm x y z) (a (x * (y * z))) =
a (x * (z * y))
forall b : G * G * G,
transport
  (fun
     w : Coeq
           (uncurry2 (fun a b0 c : G => a * (b0 * c)))
           (uncurry2 (fun a b0 c : G => a * (c * b0)))
   => P (tr w)) (cglue b)
  (?coeq'
     (uncurry2 (fun a b0 c : G => a * (b0 * c)) b)) =
?coeq' (uncurry2 (fun a b0 c : G => a * (c * b0)) b)
    1: exact a.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (abel_in x)
c: forall x y z : G,
transport P (abel_in_comm x y z) (a (x * (y * z))) =
a (x * (z * y))
forall b : G * G * G,
transport
  (fun
     w : Coeq
           (uncurry2 (fun a b0 c : G => a * (b0 * c)))
           (uncurry2 (fun a b0 c : G => a * (c * b0)))
   => P (tr w)) (cglue b)
  (a (uncurry2 (fun a b0 c : G => a * (b0 * c)) b)) =
a (uncurry2 (fun a b0 c : G => a * (c * b0)) b)
    intros [[x y] z].
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (abel_in x)
c: forall x y z : G,
transport P (abel_in_comm x y z) (a (x * (y * z))) =
a (x * (z * y))
x, y, z: G
transport
  (fun
     w : Coeq
           (uncurry2 (fun a b c : G => a * (b * c)))
           (uncurry2 (fun a b c : G => a * (c * b)))
   => P (tr w)) (cglue (x, y, z))
  (a
     (uncurry2 (fun a b c : G => a * (b * c))
        (x, y, z))) =
a (uncurry2 (fun a b c : G => a * (c * b)) (x, y, z))
    nrefine (transport_compose _ _ _ _ @ _).
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (abel_in x)
c: forall x y z : G,
transport P (abel_in_comm x y z) (a (x * (y * z))) =
a (x * (z * y))
x, y, z: G
transport P (ap tr (cglue (x, y, z)))
  (a
     (uncurry2 (fun a b c : G => a * (b * c))
        (x, y, z))) =
a (uncurry2 (fun a b c : G => a * (c * b)) (x, y, z))
    apply c.
  Defined.

  (** The computation rule on point constructors holds definitionally. *)
  Definition Abel_ind_beta_abel_in (P : Abel -> Type) `{forall x, IsHSet (P x)}
    (a : forall x, P (abel_in x))
    (c : forall x y z, DPath P (abel_in_comm x y z) (a (x * (y * z))) (a (x * (z * y))))
    (x : G)
    : Abel_ind P a c (abel_in x) = a x
    := idpath.

  (** The computation rule on paths. *)
  Definition Abel_ind_beta_abel_in_comm (P : Abel -> Type) `{forall x, IsHSet (P x)}
    (a : forall x, P (abel_in x))
    (c : forall x y z, abel_in_comm x y z # a (x * (y * z)) = a (x * (z * y)))
    (x y z : G)
    : apD (Abel_ind P a c) (abel_in_comm x y z) = c x y z.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (abel_in x)
c: forall x y z : G,
transport P (abel_in_comm x y z) (a (x * (y * z))) =
a (x * (z * y))
x, y, z: G
apD (Abel_ind P a c) (abel_in_comm x y z) = c x y z
  Proof.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (abel_in x)
c: forall x y z : G,
transport P (abel_in_comm x y z) (a (x * (y * z))) =
a (x * (z * y))
x, y, z: G
apD (Abel_ind P a c) (abel_in_comm x y z) = c x y z
    nrefine (apD_compose' tr _ _ @ ap _ _ @ concat_V_pp _ _).
G: Group
P: Abel -> Type
H: forall x : Abel, IsHSet (P x)
a: forall x : G, P (abel_in x)
c: forall x y z : G,
transport P (abel_in_comm x y z) (a (x * (y * z))) =
a (x * (z * y))
x, y, z: G
apD
  (fun
     x : Coeq
           (uncurry2 (fun a b c : G => a * (b * c)))
           (uncurry2 (fun a b c : G => a * (c * b)))
   => Abel_ind P a c (tr x)) (cglue (x, y, z)) =
transport_compose P tr (cglue (x, y, z))
  (Abel_ind P a c (tr (coeq (x * (y * z))))) @ c x y z
    rapply Coeq_ind_beta_cglue.
  Defined.

  (** We also have a recursion principle. *)
  Definition Abel_rec (P : Type) `{IsHSet P} (a : G -> P)
    (c : forall x y z, a (x * (y * z)) = a (x * (z * y)))
    : Abel -> P.
G: Group
P: Type
IsHSet0: IsHSet P
a: G -> P
c: forall x y z : G,
a (x * (y * z)) = a (x * (z * y))
Abel -> P
  Proof.
G: Group
P: Type
IsHSet0: IsHSet P
a: G -> P
c: forall x y z : G,
a (x * (y * z)) = a (x * (z * y))
Abel -> P
    apply (Abel_ind _ a).
G: Group
P: Type
IsHSet0: IsHSet P
a: G -> P
c: forall x y z : G,
a (x * (y * z)) = a (x * (z * y))
forall x y z : G,
transport (fun _ : Abel => P) (abel_in_comm x y z)
  (a (x * (y * z))) = a (x * (z * y))
    intros; apply dp_const, c.
  Defined.

  (** Here is a simpler version of [Abel_ind] when our target is an [HProp]. This lets us discard all the higher paths. *)
  Definition Abel_ind_hprop (P : Abel -> Type) `{forall x, IsHProp (P x)} 
    (a : forall x, P (abel_in x))
    : forall (x : Abel), P x.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHProp (P x)
a: forall x : G, P (abel_in x)
forall x : Abel, P x
  Proof.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHProp (P x)
a: forall x : G, P (abel_in x)
forall x : Abel, P x
    srapply Trunc_ind.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHProp (P x)
a: forall x : G, P (abel_in x)
forall
a : Coeq (uncurry2 (fun a b c : G => a * (b * c)))
      (uncurry2 (fun a b c : G => a * (c * b))),
P (tr a)
    srapply Coeq_ind_hprop.
G: Group
P: Abel -> Type
H: forall x : Abel, IsHProp (P x)
a: forall x : G, P (abel_in x)
forall a : G,
(fun
   x : Coeq
         (uncurry2 (fun a0 b c : G => a0 * (b * c)))
         (uncurry2 (fun a0 b c : G => a0 * (c * b)))
 => P (tr x)) (coeq a)
    exact a.
  Defined.

End Abel.

(** The [IsHProp] argument of [Abel_ind_hprop] can usually be found by typeclass resolution, but [srapply] is slow, so we use this tactic instead. *)
Local Ltac Abel_ind_hprop x := snapply Abel_ind_hprop; [exact _ | intro x].

(** We make sure that [G] is implicit in the arguments of [abel_in]
 and [abel_in_comm]. *)
Arguments abel_in {_} g%_mc_mult_scope.
Arguments abel_in_comm {_} (a b c)%_mc_mult_scope.

(** Now we can show that [Abel G] is in fact an abelian group. We will denote the operation in [Abel G] by the multiplicative [*] notation even though it is later shown to be commutative. *)

Section AbelGroup.

  Context (G : Group).

  (** Firstly we define the operation on [Abel G]. This is defined as follows:
<<
        abel_in x * abel_in y := abel_in (x * y)
>>
      But we need to also check that it preserves [ab_comm] in the appropriate way. *)
  #[export] Instance sgop_abel : SgOp (Abel G).
G: Group
SgOp (Abel G)
  Proof.
G: Group
SgOp (Abel G)
    intro a.
G: Group
a: Abel G
Abel G -> Abel G
    srapply Abel_rec.
G: Group
a: Abel G
G -> Abel G
G: Group
a: Abel G
forall x y z : G, ?a (x * (y * z)) = ?a (x * (z * y))
    {
G: Group
a: Abel G
G -> Abel G intro b.
G: Group
a: Abel G
b: G
Abel G
      revert a.
G: Group
b: G
Abel G -> Abel G
      srapply Abel_rec.
G: Group
b: G
G -> Abel G
G: Group
b: G
forall x y z : G, ?a (x * (y * z)) = ?a (x * (z * y))
      {
G: Group
b: G
G -> Abel G intro a.
G: Group
b, a: G
Abel G
        exact (abel_in (a * b)). }
G: Group
b: G
forall x y z : G,
(fun a : G => abel_in (a * b)) (x * (y * z)) =
(fun a : G => abel_in (a * b)) (x * (z * y))
      intros a c d; hnf.
G: Group
b, a, c, d: G
abel_in (a * (c * d) * b) = abel_in (a * (d * c) * b)
      (* The pattern seems to be to alternate [associativity] and [ab_comm]. *)
      refine (ap _ (associativity _ _ _)^ @ _).
G: Group
b, a, c, d: G
abel_in (a * (c * d * b)) = abel_in (a * (d * c) * b)
      refine (abel_in_comm _ _ _ @ _).
G: Group
b, a, c, d: G
abel_in (a * (b * (c * d))) =
abel_in (a * (d * c) * b)
      refine (ap _ (associativity _ _ _) @ _).
G: Group
b, a, c, d: G
abel_in (a * b * (c * d)) = abel_in (a * (d * c) * b)
      refine (abel_in_comm _ _ _ @ _).
G: Group
b, a, c, d: G
abel_in (a * b * (d * c)) = abel_in (a * (d * c) * b)
      refine (ap _ (associativity _ _ _)^ @ _).
G: Group
b, a, c, d: G
abel_in (a * (b * (d * c))) =
abel_in (a * (d * c) * b)
      refine (abel_in_comm _ _ _ @ _).
G: Group
b, a, c, d: G
abel_in (a * (d * c * b)) = abel_in (a * (d * c) * b)
      exact (ap _ (associativity _ _ _)). }
G: Group
a: Abel G
forall x y z : G,
(fun b : G =>
 Abel_rec G (Abel G) (fun a : G => abel_in (a * b))
   (fun a c d : G =>
    ap abel_in (associativity a (c * d) b)^ @
    (abel_in_comm a (c * d) b @
     (ap abel_in (associativity a b (c * d)) @
      (abel_in_comm (a * b) c d @
       (ap abel_in (associativity a b (d * c))^ @
        (abel_in_comm a b (d * c) @
         ap abel_in (associativity a (d * c) b))))))
    :
    (fun a0 : G => abel_in (a0 * b)) (a * (c * d)) =
    (fun a0 : G => abel_in (a0 * b)) (a * (d * c))) a)
  (x * (y * z)) =
(fun b : G =>
 Abel_rec G (Abel G) (fun a : G => abel_in (a * b))
   (fun a c d : G =>
    ap abel_in (associativity a (c * d) b)^ @
    (abel_in_comm a (c * d) b @
     (ap abel_in (associativity a b (c * d)) @
      (abel_in_comm (a * b) c d @
       (ap abel_in (associativity a b (d * c))^ @
        (abel_in_comm a b (d * c) @
         ap abel_in (associativity a (d * c) b))))))
    :
    (fun a0 : G => abel_in (a0 * b)) (a * (c * d)) =
    (fun a0 : G => abel_in (a0 * b)) (a * (d * c))) a)
  (x * (z * y))
    intros b c d.
G: Group
a: Abel G
b, c, d: G
(fun b : G =>
 Abel_rec G (Abel G) (fun a : G => abel_in (a * b))
   (fun a c d : G =>
    ap abel_in (associativity a (c * d) b)^ @
    (abel_in_comm a (c * d) b @
     (ap abel_in (associativity a b (c * d)) @
      (abel_in_comm (a * b) c d @
       (ap abel_in (associativity a b (d * c))^ @
        (abel_in_comm a b (d * c) @
         ap abel_in (associativity a (d * c) b))))))
    :
    (fun a0 : G => abel_in (a0 * b)) (a * (c * d)) =
    (fun a0 : G => abel_in (a0 * b)) (a * (d * c))) a)
  (b * (c * d)) =
(fun b : G =>
 Abel_rec G (Abel G) (fun a : G => abel_in (a * b))
   (fun a c d : G =>
    ap abel_in (associativity a (c * d) b)^ @
    (abel_in_comm a (c * d) b @
     (ap abel_in (associativity a b (c * d)) @
      (abel_in_comm (a * b) c d @
       (ap abel_in (associativity a b (d * c))^ @
        (abel_in_comm a b (d * c) @
         ap abel_in (associativity a (d * c) b))))))
    :
    (fun a0 : G => abel_in (a0 * b)) (a * (c * d)) =
    (fun a0 : G => abel_in (a0 * b)) (a * (d * c))) a)
  (b * (d * c))
    revert a.
G: Group
b, c, d: G
forall a : Abel G,
(fun b : G =>
 Abel_rec G (Abel G) (fun a0 : G => abel_in (a0 * b))
   (fun a0 c d : G =>
    ap abel_in (associativity a0 (c * d) b)^ @
    (abel_in_comm a0 (c * d) b @
     (ap abel_in (associativity a0 b (c * d)) @
      (abel_in_comm (a0 * b) c d @
       (ap abel_in (associativity a0 b (d * c))^ @
        (abel_in_comm a0 b (d * c) @
         ap abel_in (associativity a0 (d * c) b))))))
    :
    (fun a1 : G => abel_in (a1 * b)) (a0 * (c * d)) =
    (fun a1 : G => abel_in (a1 * b)) (a0 * (d * c))) a)
  (b * (c * d)) =
(fun b : G =>
 Abel_rec G (Abel G) (fun a0 : G => abel_in (a0 * b))
   (fun a0 c d : G =>
    ap abel_in (associativity a0 (c * d) b)^ @
    (abel_in_comm a0 (c * d) b @
     (ap abel_in (associativity a0 b (c * d)) @
      (abel_in_comm (a0 * b) c d @
       (ap abel_in (associativity a0 b (d * c))^ @
        (abel_in_comm a0 b (d * c) @
         ap abel_in (associativity a0 (d * c) b))))))
    :
    (fun a1 : G => abel_in (a1 * b)) (a0 * (c * d)) =
    (fun a1 : G => abel_in (a1 * b)) (a0 * (d * c))) a)
  (b * (d * c))
    Abel_ind_hprop a; simpl.
G: Group
b, c, d, a: G
abel_in (a * (b * (c * d))) =
abel_in (a * (b * (d * c)))
    refine (ap _ (associativity _ _ _) @ _).
G: Group
b, c, d, a: G
abel_in (a * b * (c * d)) =
abel_in (a * (b * (d * c)))
    refine (abel_in_comm _ _ _ @ _).
G: Group
b, c, d, a: G
abel_in (a * b * (d * c)) =
abel_in (a * (b * (d * c)))
    exact (ap _ (associativity _ _ _)^).
  Defined.

  (** We can now easily show that this operation is associative by [associativity] in [G] and the fact that being associative is a proposition. *)
  #[export] Instance associative_abel_sgop : Associative (.*.).
G: Group
Associative sg_op
  Proof.
G: Group
Associative sg_op
    intros x y.
G: Group
x, y: Abel G
forall z : Abel G, x * (y * z) = x * y * z
    Abel_ind_hprop z; revert y.
G: Group
x: Abel G
z: G
forall y : Abel G,
(fun x0 : Abel G => x * (y * x0) = x * y * x0)
  (abel_in z)
    Abel_ind_hprop y; revert x.
G: Group
z, y: G
forall x : Abel G,
(fun x0 : Abel G =>
 (fun x1 : Abel G => x * (x0 * x1) = x * x0 * x1)
   (abel_in z)) (abel_in y)
    Abel_ind_hprop x; simpl.
G: Group
z, y, x: G
abel_in x * (abel_in y * abel_in z) =
abel_in x * abel_in y * abel_in z
    napply (ap abel_in); apply associativity.
  Defined.

  (** From this we know that [Abel G] is a semigroup. *)
  #[export] Instance issemigroup_abel : IsSemiGroup (Abel G) := {}.

  (** We define the group unit as [abel_in] of the unit of [G] *)
  #[export] Instance monunit_abel_zero : MonUnit (Abel G) := abel_in mon_unit.

  (** By using Abel_ind_hprop we can prove the left and right identity laws. *)
  #[export] Instance leftidentity_abel : LeftIdentity (.*.) 1.
G: Group
LeftIdentity sg_op 1
  Proof.
G: Group
LeftIdentity sg_op 1
    Abel_ind_hprop x; cbn beta.
G: Group
x: G
1 * abel_in x = abel_in x
    napply (ap abel_in); apply left_identity.
  Defined.

  #[export] Instance rightidentity_abel : RightIdentity (.*.) 1.
G: Group
RightIdentity sg_op 1
  Proof.
G: Group
RightIdentity sg_op 1
    Abel_ind_hprop x; cbn beta.
G: Group
x: G
abel_in x * 1 = abel_in x
    napply (ap abel_in); apply right_identity.
  Defined.

  (** Hence [Abel G] is a monoid *)
  #[export] Instance ismonoid_abel : IsMonoid (Abel G) := {}.

  (** We can also prove that the operation is commutative! This will come in handy later. *)
  #[export] Instance commutative_abel : Commutative (.*.).
G: Group
Commutative sg_op
  Proof.
G: Group
Commutative sg_op
    intro x.
G: Group
x: Abel G
forall y : Abel G, x * y = y * x
    Abel_ind_hprop y.
G: Group
x: Abel G
y: G
(fun x0 : Abel G => x * x0 = x0 * x) (abel_in y)
    revert x.
G: Group
y: G
forall x : Abel G,
(fun x0 : Abel G => x * x0 = x0 * x) (abel_in y)
    Abel_ind_hprop x; cbn beta.
G: Group
y, x: G
abel_in x * abel_in y = abel_in y * abel_in x
    refine ((ap abel_in (left_identity _))^ @ _).
G: Group
y, x: G
abel_in (1 * (x * y)) = abel_in y * abel_in x
    refine (_ @ (ap abel_in (left_identity _))).
G: Group
y, x: G
abel_in (1 * (x * y)) = abel_in (1 * (y * x))
    apply abel_in_comm.
  Defined.

  (** Now we can define the inverse operation. This is just
<<
        (abel_in g)^ := abel_in g^
>>
      However when checking that it respects [ab_comm] we have to show the following:
<<
        abel_in (z^ * y^ * x^) = abel_in (y^ * z^ * x^)
>>
      there is no obvious way to do this, but we note that [abel_in (x * y)] is exactly the definition of [abel_in x * abel_in y]! Hence by [commutativity] we can show this. *)
  #[export] Instance inverse_abel : Inverse (Abel G).
G: Group
Inverse (Abel G)
  Proof.
G: Group
Inverse (Abel G)
    srapply (Abel_rec _ _ (abel_in o inv)).
G: Group
forall x y z : G,
(abel_in o inv) (x * (y * z)) =
(abel_in o inv) (x * (z * y))
    intros x y z; cbn beta.
G: Group
x, y, z: G
abel_in (x * (y * z))^ = abel_in (x * (z * y))^
    lhs napply ap.
G: Group
x, y, z: G
(x * (y * z))^ = ?Goal
G: Group
x, y, z: G
abel_in ?Goal = abel_in (x * (z * y))^
    2: rhs napply ap.
G: Group
x, y, z: G
(x * (y * z))^ = ?Goal
G: Group
x, y, z: G
abel_in ?Goal = abel_in ?Goal1
G: Group
x, y, z: G
(x * (z * y))^ = ?Goal1
    1,3: lhs rapply inverse_sg_op; napply (ap (.* _)); rapply inverse_sg_op.
G: Group
x, y, z: G
abel_in (z^ * y^ * x^) = abel_in (y^ * z^ * x^)
    change (abel_in z^ * abel_in y^ * abel_in x^
      = abel_in y^ * abel_in z^ * abel_in x^).
G: Group
x, y, z: G
abel_in z^ * abel_in y^ * abel_in x^ =
abel_in y^ * abel_in z^ * abel_in x^
    apply (ap (.* _)).
G: Group
x, y, z: G
abel_in z^ * abel_in y^ = abel_in y^ * abel_in z^
    exact (commutativity (abel_in z^) (abel_in y^)).
  Defined.

  (** Again by [Abel_ind_hprop] and the corresponding laws for [G] we can prove the left and right inverse laws. *)
  #[export] Instance leftinverse_abel : LeftInverse (.*.) (^) 1.
G: Group
LeftInverse sg_op inv 1
  Proof.
G: Group
LeftInverse sg_op inv 1
    Abel_ind_hprop x; simpl.
G: Group
x: G
(abel_in x)^ * abel_in x = 1
    napply (ap abel_in); apply left_inverse.
  Defined.

  Instance rightinverse_abel : RightInverse (.*.) (^) 1.
G: Group
RightInverse sg_op inv 1
  Proof.
G: Group
RightInverse sg_op inv 1
    Abel_ind_hprop x; simpl.
G: Group
x: G
abel_in x * (abel_in x)^ = 1
    napply (ap abel_in); apply right_inverse.
  Defined.

  (** Thus [Abel G] is a group *)
  #[export] Instance isgroup_abel : IsGroup (Abel G) := {}.

  (** And furthermore, since the operation is commutative, it is an abelian group. *)
  #[export] Instance isabgroup_abel : IsAbGroup (Abel G) := {}.

  (** By definition, the map [abel_in] is also a group homomorphism. *)
  #[export] Instance issemigrouppreserving_abel_in : IsSemiGroupPreserving abel_in.
G: Group
IsSemiGroupPreserving abel_in
  Proof.
G: Group
IsSemiGroupPreserving abel_in
    by unfold IsSemiGroupPreserving.
  Defined.

End AbelGroup.

(** We can easily prove that [abel_in] is a surjection. *)
Instance issurj_abel_in {G : Group} : IsSurjection (@abel_in G).
G: Group
IsConnMap (Tr (-1)) abel_in
Proof.
G: Group
IsConnMap (Tr (-1)) abel_in
  apply BuildIsSurjection.
G: Group
forall b : Abel G, merely (hfiber abel_in b)
  Abel_ind_hprop x; cbn beta.
G: Group
x: G
merely (hfiber abel_in (abel_in x))
  apply tr.
G: Group
x: G
hfiber abel_in (abel_in x)
  exists x.
G: Group
x: G
abel_in x = abel_in x
  reflexivity.
Defined.

(** Now we finally check that our definition of abelianization satisfies the universal property of being an abelianization. *)

(** We define [abel] to be the abelianization of a group. This is a map from [Group] to [AbGroup]. *)
Definition abel : Group -> AbGroup.
Group -> AbGroup
Proof.
Group -> AbGroup
  intro G.
G: Group
AbGroup
  snapply Build_AbGroup.
G: Group
Group
G: Group
Commutative sg_op
  -
G: Group
Group srapply (Build_Group (Abel G)).
  -
G: Group
Commutative sg_op exact _.
Defined.

(** We don't wish for [abel G] to be unfolded when using [simpl] or [cbn]. *)
Arguments abel G : simpl never.

(** The unit of this map is the map [abel_in] which typeclasses can pick up to be a homomorphism. We write it out explicitly here. *)
Definition abel_unit {G : Group} : G $-> abel G
  := @Build_GroupHomomorphism G (abel G) abel_in _.

Definition grp_homo_abel_rec {G : Group} {A : AbGroup} (f : G $-> A)
  : abel G $-> A.
G: Group
A: AbGroup
f: G $-> A
abel G $-> A
Proof.
G: Group
A: AbGroup
f: G $-> A
abel G $-> A
  snapply Build_GroupHomomorphism.
G: Group
A: AbGroup
f: G $-> A
abel G -> A
G: Group
A: AbGroup
f: G $-> A
IsSemiGroupPreserving ?grp_homo_map
  {
G: Group
A: AbGroup
f: G $-> A
abel G -> A srapply (Abel_rec _ _ f).
G: Group
A: AbGroup
f: G $-> A
forall x y z : G, f (x * (y * z)) = f (x * (z * y))
    intros x y z.
G: Group
A: AbGroup
f: G $-> A
x, y, z: G
f (x * (y * z)) = f (x * (z * y))
    napply grp_homo_op_agree; trivial.
G: Group
A: AbGroup
f: G $-> A
x, y, z: G
f (y * z) = f (z * y)
    refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^).
G: Group
A: AbGroup
f: G $-> A
x, y, z: G
f y * f z = f z * f y
    apply commutativity. }
G: Group
A: AbGroup
f: G $-> A
IsSemiGroupPreserving
  (Abel_rec G A f
     (fun x y z : G =>
      grp_homo_op_agree f f 1
        ((grp_homo_op f y z @
          commutativity (f y) (f z)) @
         (grp_homo_op f z y)^)))
  intros y.
G: Group
A: AbGroup
f: G $-> A
y: abel G
forall y0 : abel G,
Abel_rec G A f
  (fun x y z : G =>
   grp_homo_op_agree f f 1
     ((grp_homo_op f y z @ commutativity (f y) (f z)) @
      (grp_homo_op f z y)^)) (y * y0) =
Abel_rec G A f
  (fun x y z : G =>
   grp_homo_op_agree f f 1
     ((grp_homo_op f y z @ commutativity (f y) (f z)) @
      (grp_homo_op f z y)^)) y *
Abel_rec G A f
  (fun x y z : G =>
   grp_homo_op_agree f f 1
     ((grp_homo_op f y z @ commutativity (f y) (f z)) @
      (grp_homo_op f z y)^)) y0
  Abel_ind_hprop x; revert y.
G: Group
A: AbGroup
f: G $-> A
x: G
forall y : abel G,
(fun x : Abel G =>
 Abel_rec G A f
   (fun x0 y0 z : G =>
    grp_homo_op_agree f f 1
      ((grp_homo_op f y0 z @
        commutativity (f y0) (f z)) @
       (grp_homo_op f z y0)^)) (y * x) =
 Abel_rec G A f
   (fun x0 y0 z : G =>
    grp_homo_op_agree f f 1
      ((grp_homo_op f y0 z @
        commutativity (f y0) (f z)) @
       (grp_homo_op f z y0)^)) y *
 Abel_rec G A f
   (fun x0 y0 z : G =>
    grp_homo_op_agree f f 1
      ((grp_homo_op f y0 z @
        commutativity (f y0) (f z)) @
       (grp_homo_op f z y0)^)) x) (abel_in x)
  Abel_ind_hprop y.
G: Group
A: AbGroup
f: G $-> A
x, y: G
(fun x0 : Abel G =>
 (fun x : Abel G =>
  Abel_rec G A f
    (fun x1 y z : G =>
     grp_homo_op_agree f f 1
       ((grp_homo_op f y z @ commutativity (f y) (f z)) @
        (grp_homo_op f z y)^)) (x0 * x) =
  Abel_rec G A f
    (fun x1 y z : G =>
     grp_homo_op_agree f f 1
       ((grp_homo_op f y z @ commutativity (f y) (f z)) @
        (grp_homo_op f z y)^)) x0 *
  Abel_rec G A f
    (fun x1 y z : G =>
     grp_homo_op_agree f f 1
       ((grp_homo_op f y z @ commutativity (f y) (f z)) @
        (grp_homo_op f z y)^)) x) (abel_in x))
  (abel_in y)
  apply grp_homo_op.
Defined.

Definition abel_ind_homotopy {G H : Group} {f g : Hom (A:=Group) (abel G) H}
  (p : f $o abel_unit $== g $o abel_unit)
  : f $== g.
G, H: Group
f, g: abel G $-> H
p: f $o abel_unit $== g $o abel_unit
f $== g
Proof.
G, H: Group
f, g: abel G $-> H
p: f $o abel_unit $== g $o abel_unit
f $== g
  rapply Abel_ind_hprop.
G, H: Group
f, g: abel G $-> H
p: f $o abel_unit $== g $o abel_unit
forall x : G, f (abel_in x) = g (abel_in x)
  exact p.
Defined.

(** Finally we can prove that our construction abel is an abelianization. *)
Instance isabelianization_abel {G : Group}
  : IsAbelianization (abel G) abel_unit.
G: Group
IsAbelianization (abel G) abel_unit
Proof.
G: Group
IsAbelianization (abel G) abel_unit
  intros A.
G: Group
A: AbGroup
IsSurjInj (group_precomp A abel_unit) constructor.
G: Group
A: AbGroup
SplEssSurj (group_precomp A abel_unit)
G: Group
A: AbGroup
forall x y : abel G $-> A,
group_precomp A abel_unit x $==
group_precomp A abel_unit y -> x $== y
  {
G: Group
A: AbGroup
SplEssSurj (group_precomp A abel_unit) intros h.
G: Group
A: AbGroup
h: G $-> A
{a : abel G $-> A & group_precomp A abel_unit a $== h}
    snrefine (grp_homo_abel_rec h; _).
G: Group
A: AbGroup
h: G $-> A
(fun a : abel G $-> A =>
 group_precomp A abel_unit a $== h)
  (grp_homo_abel_rec h)
    cbn.
G: Group
A: AbGroup
h: G $-> A
(fun x : G =>
 Coeq_ind
   (fun
      _ : Coeq
            (uncurry2 (fun a b c : G => a * (b * c)))
            (uncurry2 (fun a b c : G => a * (c * b)))
    => A) h
   (fun b : G * G * G =>
    transport_compose
      (fun
         _ : Trunc 0
               (Coeq
                  (uncurry2
                     (fun a b0 c : G => a * (b0 * c)))
                  (uncurry2
                     (fun a b0 c : G => a * (c * b0))))
       => A) tr
      (cglue (fst (fst b), snd (fst b), snd b))
      (h
         (uncurry2 (fun a b0 c : G => a * (b0 * c))
            (fst (fst b), snd (fst b), snd b))) @
    dp_const
      (grp_homo_op_agree h h 1
         ((grp_homo_op h (snd (fst b)) (snd b) @
           commutativity (h (snd (fst b))) (h (snd b))) @
          (grp_homo_op h (snd b) (snd (fst b)))^)))
   (coeq x)) == h reflexivity. }
G: Group
A: AbGroup
forall x y : abel G $-> A,
group_precomp A abel_unit x $==
group_precomp A abel_unit y -> x $== y
  intros g h p.
G: Group
A: AbGroup
g, h: abel G $-> A
p: group_precomp A abel_unit g $==
group_precomp A abel_unit h
g $== h
  Abel_ind_hprop x.
G: Group
A: AbGroup
g, h: abel G $-> A
p: group_precomp A abel_unit g $==
group_precomp A abel_unit h
x: G
(fun x : Abel G =>
 (grp_homo_map
  :
  GroupHomomorphism (abel G) A -> abel G $-> A) g x =
 (grp_homo_map
  :
  GroupHomomorphism (abel G) A -> abel G $-> A) h x)
  (abel_in x)
  exact (p x).
Defined.

Theorem groupiso_isabelianization {G : Group}
  (A B : AbGroup)
  (eta1 : GroupHomomorphism G A)
  (eta2 : GroupHomomorphism G B)
  {isab1 : IsAbelianization A eta1}
  {isab2 : IsAbelianization B eta2}
  : A ≅ B.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
A ≅ B
Proof.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
A ≅ B
  destruct (esssurj (group_precomp B eta1) eta2) as [a ac].
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
A ≅ B
  destruct (esssurj (group_precomp A eta2) eta1) as [b bc].
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
A ≅ B
  srapply (Build_GroupIsomorphism _ _ a).
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
IsEquiv a
  srapply (isequiv_adjointify _ b).
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
a o b == idmap
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
b o a == idmap
  {
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
a o b == idmap refine (essinj (group_precomp B eta2)
                   (x := a $o b) (y := Id (A := Group) B) _).
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
group_precomp B eta2 (a $o b) $==
group_precomp B eta2 (Id B)
    intros x; cbn in *.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: GroupHomomorphism A B
ac: (fun x : G => a (eta1 x)) == eta2
b: GroupHomomorphism B A
bc: (fun x : G => b (eta2 x)) == eta1
x: G
a (b (eta2 x)) = eta2 x
    refine (_ @ ac x).
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: GroupHomomorphism A B
ac: (fun x : G => a (eta1 x)) == eta2
b: GroupHomomorphism B A
bc: (fun x : G => b (eta2 x)) == eta1
x: G
a (b (eta2 x)) = a (eta1 x)
    apply ap, bc. }
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
b o a == idmap
  {
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
b o a == idmap refine (essinj (group_precomp A eta1)
                   (x := b $o a) (y := Id (A := Group) A) _).
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: A $-> B
ac: group_precomp B eta1 a $== eta2
b: B $-> A
bc: group_precomp A eta2 b $== eta1
group_precomp A eta1 (b $o a) $==
group_precomp A eta1 (Id A)
    intros x; cbn in *.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: GroupHomomorphism A B
ac: (fun x : G => a (eta1 x)) == eta2
b: GroupHomomorphism B A
bc: (fun x : G => b (eta2 x)) == eta1
x: G
b (a (eta1 x)) = eta1 x
    refine (_ @ bc x).
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
a: GroupHomomorphism A B
ac: (fun x : G => a (eta1 x)) == eta2
b: GroupHomomorphism B A
bc: (fun x : G => b (eta2 x)) == eta1
x: G
b (a (eta1 x)) = b (eta2 x)
    apply ap, ac. }
Defined.

Theorem homotopic_isabelianization {G : Group} (A B : AbGroup)
  (eta1 : GroupHomomorphism G A) (eta2 : GroupHomomorphism G B)
  {isab1 : IsAbelianization A eta1} {isab2 : IsAbelianization B eta2}
  : eta2 == grp_homo_compose (groupiso_isabelianization A B eta1 eta2) eta1.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
eta2 ==
grp_homo_compose
  (groupiso_isabelianization A B eta1 eta2) eta1
Proof.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
eta2 ==
grp_homo_compose
  (groupiso_isabelianization A B eta1 eta2) eta1
  intros x.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
x: G
eta2 x =
grp_homo_compose
  (groupiso_isabelianization A B eta1 eta2) eta1 x
  symmetry.
G: Group
A, B: AbGroup
eta1: GroupHomomorphism G A
eta2: GroupHomomorphism G B
isab1: IsAbelianization A eta1
isab2: IsAbelianization B eta2
x: G
grp_homo_compose
  (groupiso_isabelianization A B eta1 eta2) eta1 x =
eta2 x
  exact ((esssurj (group_precomp B eta1) eta2).2 x).
Defined.

(** Hence any abelianization is surjective. *)
Instance issurj_isabelianization {G : Group}
  (A : AbGroup) (eta : GroupHomomorphism G A)
  : IsAbelianization A eta -> IsSurjection eta.
G: Group
A: AbGroup
eta: GroupHomomorphism G A
IsAbelianization A eta -> IsConnMap (Tr (-1)) eta
Proof.
G: Group
A: AbGroup
eta: GroupHomomorphism G A
IsAbelianization A eta -> IsConnMap (Tr (-1)) eta
  intros k.
G: Group
A: AbGroup
eta: GroupHomomorphism G A
k: IsAbelianization A eta
IsConnMap (Tr (-1)) eta
  pose (homotopic_isabelianization A (abel G) eta abel_unit) as p.
G: Group
A: AbGroup
eta: GroupHomomorphism G A
k: IsAbelianization A eta
p:= homotopic_isabelianization A (abel G) eta abel_unit: abel_unit ==
grp_homo_compose
  (groupiso_isabelianization A (abel G) eta
     abel_unit) eta
IsConnMap (Tr (-1)) eta
  exact (@cancelL_isequiv_conn_map _ _ _ _ _ _ _
    (conn_map_homotopic _ _ _ p _)).
Defined.

Instance isabelianization_identity (A : AbGroup) : IsAbelianization A grp_homo_id.
A: AbGroup
IsAbelianization A grp_homo_id
Proof.
A: AbGroup
IsAbelianization A grp_homo_id
  intros B.
A, B: AbGroup
IsSurjInj (group_precomp B grp_homo_id) constructor.
A, B: AbGroup
SplEssSurj (group_precomp B grp_homo_id)
A, B: AbGroup
forall x y : A $-> B,
group_precomp B grp_homo_id x $==
group_precomp B grp_homo_id y -> x $== y
  -
A, B: AbGroup
SplEssSurj (group_precomp B grp_homo_id) intros h; exact (h ; fun _ => idpath).
  -
A, B: AbGroup
forall x y : A $-> B,
group_precomp B grp_homo_id x $==
group_precomp B grp_homo_id y -> x $== y intros g h p; exact p.
Defined.

Instance isequiv_abgroup_abelianization
  (A B : AbGroup) (eta : GroupHomomorphism A B) {isab : IsAbelianization B eta}
  : IsEquiv eta.
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
IsEquiv eta
Proof.
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
IsEquiv eta
  srapply isequiv_homotopic.
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
A -> B
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
IsEquiv ?f
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
?f == eta
  -
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
A -> B exact (groupiso_isabelianization A B grp_homo_id eta).
  -
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
IsEquiv
  (groupiso_isabelianization A B grp_homo_id eta) exact _.
  -
A, B: AbGroup
eta: GroupHomomorphism A B
isab: IsAbelianization B eta
groupiso_isabelianization A B grp_homo_id eta == eta symmetry; apply homotopic_isabelianization.
Defined.

(** ** Functoriality *)

Instance is0functor_abel : Is0Functor abel.
Is0Functor abel
Proof.
Is0Functor abel
  snapply Build_Is0Functor.
forall a b : Group, (a $-> b) -> abel a $-> abel b
  intros A B f.
A, B: Group
f: A $-> B
abel A $-> abel B
  snapply grp_homo_abel_rec.
A, B: Group
f: A $-> B
A $-> abel B
  exact (abel_unit $o f).
Defined.

Instance is1functor_abel : Is1Functor abel.
Is1Functor abel
Proof.
Is1Functor abel
  snapply Build_Is1Functor.
forall (a b : Group) (f g : a $-> b),
f $== g -> fmap abel f $== fmap abel g
forall a : Group, fmap abel (Id a) $== Id (abel a)
forall (a b c : Group) (f : a $-> b) (g : b $-> c),
fmap abel (g $o f) $== fmap abel g $o fmap abel f
  -
forall (a b : Group) (f g : a $-> b),
f $== g -> fmap abel f $== fmap abel g intros A B f g p.
A, B: Group
f, g: A $-> B
p: f $== g
fmap abel f $== fmap abel g
    unfold abel.
A, B: Group
f, g: A $-> B
p: f $== g
fmap abel f $== fmap abel g
    rapply Abel_ind_hprop.
A, B: Group
f, g: A $-> B
p: f $== g
forall x : A,
fmap abel f (abel_in x) = fmap abel g (abel_in x)
    intros x.
A, B: Group
f, g: A $-> B
p: f $== g
x: A
fmap abel f (abel_in x) = fmap abel g (abel_in x)
    exact (ap abel_in (p x)).
  -
forall a : Group, fmap abel (Id a) $== Id (abel a) intros A.
A: Group
fmap abel (Id A) $== Id (abel A)
    by rapply Abel_ind_hprop.
  -
forall (a b c : Group) (f : a $-> b) (g : b $-> c),
fmap abel (g $o f) $== fmap abel g $o fmap abel f intros A B C f g.
A, B, C: Group
f: A $-> B
g: B $-> C
fmap abel (g $o f) $== fmap abel g $o fmap abel f
    by rapply Abel_ind_hprop.
Defined.