QuotientGroup.v

Require Import Basics Types.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.Core.
Require Import Algebra.Congruence.
Require Import Algebra.Groups.Group.
Require Import Algebra.Groups.Subgroup.
Require Export Algebra.Groups.Image.
Require Export Algebra.Groups.Kernel.
Require Export Colimits.Quotient.
Require Import HSet.
Require Import Spaces.Finite.Finite.
Require Import WildCat.
Require Import Modalities.Modality.

(** * Quotient groups *)

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

Section GroupCongruenceQuotient.

  Context {G : Group} {R : Relation G}
    `{is_mere_relation _ R, !IsCongruence R,
      !Reflexive R, !Symmetric R, !Transitive R}.

  Definition CongruenceQuotient := G / R.

  Global Instance congquot_sgop : SgOp CongruenceQuotient.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
SgOp CongruenceQuotient
  Proof.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
SgOp CongruenceQuotient
    intros x.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x: CongruenceQuotient
CongruenceQuotient -> CongruenceQuotient
    srapply Quotient_rec.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x: CongruenceQuotient
G -> CongruenceQuotient
G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x: CongruenceQuotient
forall x0 y : G, R x0 y -> ?pclass x0 = ?pclass y
    {G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x: CongruenceQuotient
G -> CongruenceQuotient intro y; revert x.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
y: G
CongruenceQuotient -> CongruenceQuotient
      srapply Quotient_rec.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
y: G
G -> CongruenceQuotient
G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
y: G
forall x y0 : G, R x y0 -> ?pclass x = ?pclass y0
      {G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
y: G
G -> CongruenceQuotient intros x.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
y, x: G
CongruenceQuotient
        apply class_of.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
y, x: G
G
        exact (x * y). }G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
y: G
forall x y0 : G,
R x y0 ->
(fun x0 : G => class_of R (x0 * y)) x =
(fun x0 : G => class_of R (x0 * y)) y0
      intros a b r.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
y, a, b: G
r: R a b
(fun x : G => class_of R (x * y)) a =
(fun x : G => class_of R (x * y)) b
      cbn.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
y, a, b: G
r: R a b
class_of R (a * y) = class_of R (b * y)
      apply qglue.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
y, a, b: G
r: R a b
R (a * y) (b * y)
      by apply iscong. }G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x: CongruenceQuotient
forall x0 y : G,
R x0 y ->
(fun y0 : G =>
 Quotient_rec R CongruenceQuotient
   (fun x : G => class_of R (x * y0))
   (fun (a b : G) (r : R a b) =>
    qglue (iscong r (Reflexive0 y0))
    :
    (fun x : G => class_of R (x * y0)) a =
    (fun x : G => class_of R (x * y0)) b) x) x0 =
(fun y0 : G =>
 Quotient_rec R CongruenceQuotient
   (fun x : G => class_of R (x * y0))
   (fun (a b : G) (r : R a b) =>
    qglue (iscong r (Reflexive0 y0))
    :
    (fun x : G => class_of R (x * y0)) a =
    (fun x : G => class_of R (x * y0)) b) x) y
    intros a b r.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x: CongruenceQuotient
a, b: G
r: R a b
(fun y : G =>
 Quotient_rec R CongruenceQuotient
   (fun x : G => class_of R (x * y))
   (fun (a b : G) (r : R a b) =>
    qglue (iscong r (Reflexive0 y))
    :
    (fun x : G => class_of R (x * y)) a =
    (fun x : G => class_of R (x * y)) b) x) a =
(fun y : G =>
 Quotient_rec R CongruenceQuotient
   (fun x : G => class_of R (x * y))
   (fun (a b : G) (r : R a b) =>
    qglue (iscong r (Reflexive0 y))
    :
    (fun x : G => class_of R (x * y)) a =
    (fun x : G => class_of R (x * y)) b) x) b
    revert x.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
a, b: G
r: R a b
forall x : CongruenceQuotient,
(fun y : G =>
 Quotient_rec R CongruenceQuotient
   (fun x0 : G => class_of R (x0 * y))
   (fun (a b : G) (r : R a b) =>
    qglue (iscong r (Reflexive0 y))
    :
    (fun x0 : G => class_of R (x0 * y)) a =
    (fun x0 : G => class_of R (x0 * y)) b) x) a =
(fun y : G =>
 Quotient_rec R CongruenceQuotient
   (fun x0 : G => class_of R (x0 * y))
   (fun (a b : G) (r : R a b) =>
    qglue (iscong r (Reflexive0 y))
    :
    (fun x0 : G => class_of R (x0 * y)) a =
    (fun x0 : G => class_of R (x0 * y)) b) x) b
    srapply Quotient_ind_hprop.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
a, b: G
r: R a b
forall x : G,
(fun q : G / R =>
 (fun y : G =>
  Quotient_rec R CongruenceQuotient
    (fun x0 : G => class_of R (x0 * y))
    (fun (a b : G) (r : R a b) =>
     qglue (iscong r (Reflexive0 y))
     :
     (fun x0 : G => class_of R (x0 * y)) a =
     (fun x0 : G => class_of R (x0 * y)) b) q) a =
 (fun y : G =>
  Quotient_rec R CongruenceQuotient
    (fun x0 : G => class_of R (x0 * y))
    (fun (a b : G) (r : R a b) =>
     qglue (iscong r (Reflexive0 y))
     :
     (fun x0 : G => class_of R (x0 * y)) a =
     (fun x0 : G => class_of R (x0 * y)) b) q) b)
  (class_of R x)
    intro x.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
a, b: G
r: R a b
x: G
(fun q : G / R =>
 (fun y : G =>
  Quotient_rec R CongruenceQuotient
    (fun x : G => class_of R (x * y))
    (fun (a b : G) (r : R a b) =>
     qglue (iscong r (Reflexive0 y))
     :
     (fun x : G => class_of R (x * y)) a =
     (fun x : G => class_of R (x * y)) b) q) a =
 (fun y : G =>
  Quotient_rec R CongruenceQuotient
    (fun x : G => class_of R (x * y))
    (fun (a b : G) (r : R a b) =>
     qglue (iscong r (Reflexive0 y))
     :
     (fun x : G => class_of R (x * y)) a =
     (fun x : G => class_of R (x * y)) b) q) b)
  (class_of R x)
    apply qglue.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
a, b: G
r: R a b
x: G
R (x * a) (x * b)
    by apply iscong.
  Defined.

  Global Instance congquot_mon_unit : MonUnit CongruenceQuotient.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
MonUnit CongruenceQuotient
  Proof.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
MonUnit CongruenceQuotient
    apply class_of, mon_unit.
  Defined.

  Global Instance congquot_negate : Negate CongruenceQuotient.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
Negate CongruenceQuotient
  Proof.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
Negate CongruenceQuotient
    srapply Quotient_functor.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
G -> G
G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
forall x y : G, R x y -> R (?f x) (?f y)
    1: apply negate.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
forall x y : G, R x y -> R (- x) (- y)
    intros x y p.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x, y: G
p: R x y
R (- x) (- y)
    rewrite <- (left_identity (-x)).G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x, y: G
p: R x y
R (mon_unit * - x) (- y)
    destruct (left_inverse y).G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x, y: G
p: R x y
R (- y * y * - x) (- y)
    set (-y * y * -x).G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x, y: G
p: R x y
g:= - y * y * - x: G
R g (- y)
    rewrite <- (right_identity (-y)).G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x, y: G
p: R x y
g:= - y * y * - x: G
R g (- y * mon_unit)
    destruct (right_inverse x).G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x, y: G
p: R x y
g:= - y * y * - x: G
R g (- y * (x * - x))
    unfold g; clear g.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x, y: G
p: R x y
R (- y * y * - x) (- y * (x * - x))
    rewrite <- simple_associativity.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x, y: G
p: R x y
R (- y * (y * - x)) (- y * (x * - x))
    apply iscong; try reflexivity.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x, y: G
p: R x y
R (y * - x) (x * - x)
    apply iscong; try reflexivity.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x, y: G
p: R x y
R y x
    by symmetry.
  Defined.

  Global Instance congquot_sgop_associative : Associative congquot_sgop.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
Associative congquot_sgop
  Proof.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
Associative congquot_sgop
    intros x y.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x, y: CongruenceQuotient
forall z : CongruenceQuotient,
congquot_sgop x (congquot_sgop y z) =
congquot_sgop (congquot_sgop x y) z
    srapply Quotient_ind_hprop; intro a; revert y.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x: CongruenceQuotient
a: G
forall y : CongruenceQuotient,
(fun q : G / R =>
 congquot_sgop x (congquot_sgop y q) =
 congquot_sgop (congquot_sgop x y) q) (class_of R a)
    srapply Quotient_ind_hprop; intro b; revert x.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
a, b: G
forall x : CongruenceQuotient,
(fun q : G / R =>
 (fun q0 : G / R =>
  congquot_sgop x (congquot_sgop q q0) =
  congquot_sgop (congquot_sgop x q) q0) (class_of R a))
  (class_of R b)
    srapply Quotient_ind_hprop; intro c.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
a, b, c: G
(fun q : G / R =>
 (fun q0 : G / R =>
  (fun q1 : G / R =>
   congquot_sgop q (congquot_sgop q0 q1) =
   congquot_sgop (congquot_sgop q q0) q1)
    (class_of R a)) (class_of R b)) (class_of R c)
    simpl; by rewrite associativity.
  Qed.

  Global Instance issemigroup_congquot : IsSemiGroup CongruenceQuotient := {}.

  Global Instance congquot_leftidentity
    : LeftIdentity congquot_sgop congquot_mon_unit.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
LeftIdentity congquot_sgop congquot_mon_unit
  Proof.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
LeftIdentity congquot_sgop congquot_mon_unit
    srapply Quotient_ind_hprop; intro x.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x: G
(fun q : G / R =>
 congquot_sgop congquot_mon_unit q = q) (class_of R x)
    by simpl; rewrite left_identity.
  Qed.

  Global Instance congquot_rightidentity
    : RightIdentity congquot_sgop congquot_mon_unit.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
RightIdentity congquot_sgop congquot_mon_unit
  Proof.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
RightIdentity congquot_sgop congquot_mon_unit
    srapply Quotient_ind_hprop; intro x.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x: G
(fun q : G / R =>
 congquot_sgop q congquot_mon_unit = q) (class_of R x)
    by simpl; rewrite right_identity.
  Qed.

  Global Instance ismonoid_quotientgroup : IsMonoid CongruenceQuotient := {}.

  Global Instance quotientgroup_leftinverse
    : LeftInverse congquot_sgop congquot_negate congquot_mon_unit.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
LeftInverse congquot_sgop congquot_negate
  congquot_mon_unit
  Proof.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
LeftInverse congquot_sgop congquot_negate
  congquot_mon_unit
    srapply Quotient_ind_hprop; intro x.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x: G
(fun q : G / R =>
 congquot_sgop (congquot_negate q) q =
 congquot_mon_unit) (class_of R x)
    by simpl; rewrite left_inverse.
  Qed.

  Global Instance quotientgroup_rightinverse
    : RightInverse congquot_sgop congquot_negate congquot_mon_unit.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
RightInverse congquot_sgop congquot_negate
  congquot_mon_unit
  Proof.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
RightInverse congquot_sgop congquot_negate
  congquot_mon_unit
    srapply Quotient_ind_hprop; intro x.G: Group
R: Relation G
is_mere_relation0: is_mere_relation G R
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Symmetric0: Symmetric R
Transitive0: Transitive R
x: G
(fun q : G / R =>
 congquot_sgop q (congquot_negate q) =
 congquot_mon_unit) (class_of R x)
    by simpl; rewrite right_inverse.
  Qed.

  Global Instance isgroup_quotientgroup : IsGroup CongruenceQuotient := {}.

End GroupCongruenceQuotient.

(** Now we can define the quotient group by a normal subgroup. *)

Section QuotientGroup.

  Context (G : Group) (N : NormalSubgroup G).

  Global Instance iscongruence_in_cosetL : IsCongruence (in_cosetL N).G: Group
N: NormalSubgroup G
IsCongruence (in_cosetL N)
  Proof.G: Group
N: NormalSubgroup G
IsCongruence (in_cosetL N)
    srapply Build_IsCongruence.G: Group
N: NormalSubgroup G
forall x x' y y' : G,
in_cosetL N x x' ->
in_cosetL N y y' -> in_cosetL N (x * y) (x' * y')
    intros; by apply in_cosetL_cong.
  Defined.

  Global Instance iscongruence_in_cosetR: IsCongruence (in_cosetR N).G: Group
N: NormalSubgroup G
IsCongruence (in_cosetR N)
  Proof.G: Group
N: NormalSubgroup G
IsCongruence (in_cosetR N)
    srapply Build_IsCongruence.G: Group
N: NormalSubgroup G
forall x x' y y' : G,
in_cosetR N x x' ->
in_cosetR N y y' -> in_cosetR N (x * y) (x' * y')
    intros; by apply in_cosetR_cong.
  Defined.

  (** Now we have to make a choice whether to pick the left or right cosets. Due to existing convention we shall pick left cosets but we note that we could equally have picked right. *)
  Definition QuotientGroup : Group
    := Build_Group (G / (in_cosetL N)) _ _ _ _.

  Definition grp_quotient_map : G $-> QuotientGroup.G: Group
N: NormalSubgroup G
G $-> QuotientGroup
  Proof.G: Group
N: NormalSubgroup G
G $-> QuotientGroup
    snrapply Build_GroupHomomorphism.G: Group
N: NormalSubgroup G
G -> QuotientGroup
G: Group
N: NormalSubgroup G
IsSemiGroupPreserving ?f
    1: exact (class_of _).G: Group
N: NormalSubgroup G
IsSemiGroupPreserving (class_of (in_cosetL N))
    intros ??; reflexivity.
  Defined.

  Definition grp_quotient_rec {A : Group} (f : G $-> A)
             (h : forall n : G, N n -> f n = mon_unit)
    : QuotientGroup $-> A.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
QuotientGroup $-> A
  Proof.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
QuotientGroup $-> A
    snrapply Build_GroupHomomorphism.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
QuotientGroup -> A
G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
IsSemiGroupPreserving ?f
    -G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
QuotientGroup -> A srapply Quotient_rec.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
G -> A
G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
forall x y : G,
in_cosetL N x y -> ?pclass x = ?pclass y
      +G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
G -> A exact f.
      +G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
forall x y : G, in_cosetL N x y -> f x = f y cbn; intros x y n.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
x, y: G
n: N (- x * y)
f x = f y
        symmetry.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
x, y: G
n: N (- x * y)
f y = f x
        apply grp_moveL_M1.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
x, y: G
n: N (- x * y)
- f x * f y = mon_unit
        rewrite <- grp_homo_inv.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
x, y: G
n: N (- x * y)
f (- x) * f y = mon_unit
        rewrite <- grp_homo_op.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
x, y: G
n: N (- x * y)
f (- x * y) = mon_unit
        apply h; assumption.
    -G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
IsSemiGroupPreserving
  (Quotient_rec (in_cosetL N) A f
     ((fun (x y : G) (n : N (- x * y)) =>
       (let X := equiv_fun grp_moveL_M1 in
        X
          (internal_paths_rew
             (fun g : A => g * f y = mon_unit)
             (internal_paths_rew
                (fun g : A => g = mon_unit)
                (h (- x * y) n)
                (grp_homo_op f (- x) y))
             (grp_homo_inv f x)))^)
      :
      forall x y : G, in_cosetL N x y -> f x = f y)) intro x.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
x: QuotientGroup
forall y : QuotientGroup,
Quotient_rec (in_cosetL N) A f
  (fun (x y0 : G) (n : N (- x * y0)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y0 = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x * y0) n) (grp_homo_op f (- x) y0))
         (grp_homo_inv f x)))^) (x * y) =
Quotient_rec (in_cosetL N) A f
  (fun (x y0 : G) (n : N (- x * y0)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y0 = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x * y0) n) (grp_homo_op f (- x) y0))
         (grp_homo_inv f x)))^) x *
Quotient_rec (in_cosetL N) A f
  (fun (x y0 : G) (n : N (- x * y0)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y0 = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x * y0) n) (grp_homo_op f (- x) y0))
         (grp_homo_inv f x)))^) y
      refine (Quotient_ind_hprop _ _ _).G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
x: QuotientGroup
forall x0 : G,
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (- x * y)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x * y) n) (grp_homo_op f (- x) y))
         (grp_homo_inv f x)))^)
  (x * class_of (in_cosetL N) x0) =
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (- x * y)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x * y) n) (grp_homo_op f (- x) y))
         (grp_homo_inv f x)))^) x *
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (- x * y)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x * y) n) (grp_homo_op f (- x) y))
         (grp_homo_inv f x)))^)
  (class_of (in_cosetL N) x0)
      intro y.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
x: QuotientGroup
y: G
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (- x * y)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x * y) n) (grp_homo_op f (- x) y))
         (grp_homo_inv f x)))^)
  (x * class_of (in_cosetL N) y) =
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (- x * y)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x * y) n) (grp_homo_op f (- x) y))
         (grp_homo_inv f x)))^) x *
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (- x * y)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x * y) n) (grp_homo_op f (- x) y))
         (grp_homo_inv f x)))^)
  (class_of (in_cosetL N) y) revert x.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
y: G
forall x : QuotientGroup,
Quotient_rec (in_cosetL N) A f
  (fun (x0 y : G) (n : N (- x0 * y)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x0 * y) n) (grp_homo_op f (- x0) y))
         (grp_homo_inv f x0)))^)
  (x * class_of (in_cosetL N) y) =
Quotient_rec (in_cosetL N) A f
  (fun (x0 y : G) (n : N (- x0 * y)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x0 * y) n) (grp_homo_op f (- x0) y))
         (grp_homo_inv f x0)))^) x *
Quotient_rec (in_cosetL N) A f
  (fun (x0 y : G) (n : N (- x0 * y)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x0 * y) n) (grp_homo_op f (- x0) y))
         (grp_homo_inv f x0)))^)
  (class_of (in_cosetL N) y)

      refine (Quotient_ind_hprop _ _ _).G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
y: G
forall x : G,
Quotient_rec (in_cosetL N) A f
  (fun (x0 y : G) (n : N (- x0 * y)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x0 * y) n) (grp_homo_op f (- x0) y))
         (grp_homo_inv f x0)))^)
  (class_of (in_cosetL N) x * class_of (in_cosetL N) y) =
Quotient_rec (in_cosetL N) A f
  (fun (x0 y : G) (n : N (- x0 * y)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x0 * y) n) (grp_homo_op f (- x0) y))
         (grp_homo_inv f x0)))^)
  (class_of (in_cosetL N) x) *
Quotient_rec (in_cosetL N) A f
  (fun (x0 y : G) (n : N (- x0 * y)) =>
   (let X := equiv_fun grp_moveL_M1 in
    X
      (internal_paths_rew
         (fun g : A => g * f y = mon_unit)
         (internal_paths_rew
            (fun g : A => g = mon_unit)
            (h (- x0 * y) n) (grp_homo_op f (- x0) y))
         (grp_homo_inv f x0)))^)
  (class_of (in_cosetL N) y)
      intro x; simpl.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
y, x: G
f (x * y) = f x * f y
      apply grp_homo_op.
  Defined.

End QuotientGroup.

Arguments grp_quotient_map {_ _}.

Notation "G / N" := (QuotientGroup G N) : group_scope.

(** Rephrasing that lets you specify the normality proof *)
Definition QuotientGroup' (G : Group) (N : Subgroup G) (H : IsNormalSubgroup N)
  := QuotientGroup G (Build_NormalSubgroup G N H).

Local Open Scope group_scope.

(** Computation rule for grp_quotient_rec. *)
Corollary grp_quotient_rec_beta `{F : Funext} {G : Group}
          (N : NormalSubgroup G) (H : Group)
          {A : Group} (f : G $-> A)
          (h : forall n:G, N n -> f n = mon_unit)
  : (grp_quotient_rec G N f h) $o grp_quotient_map = f.F: Funext
G: Group
N: NormalSubgroup G
H, A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
grp_quotient_rec G N f h $o grp_quotient_map = f
Proof.F: Funext
G: Group
N: NormalSubgroup G
H, A: Group
f: G $-> A
h: forall n : G, N n -> f n = mon_unit
grp_quotient_rec G N f h $o grp_quotient_map = f
  apply equiv_path_grouphomomorphism; reflexivity.
Defined.

(** Computation rule for grp_quotient_rec. *)
Definition grp_quotient_rec_beta' {G : Group}
          (N : NormalSubgroup G) (H : Group)
          {A : Group} (f : G $-> A)
          (h : forall n:G, N n -> f n = mon_unit)
  : (grp_quotient_rec G N f h) $o grp_quotient_map == f
    := fun _ => idpath.

(** The proof of normality is irrelevent up to equivalence. This is unfortunate that it doesn't hold definitionally. *)
Definition grp_iso_quotient_normal (G : Group) (H : Subgroup G)
  {k k' : IsNormalSubgroup H}
  : QuotientGroup' G H k ≅ QuotientGroup' G H k'.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
QuotientGroup' G H k ≅ QuotientGroup' G H k'
Proof.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
QuotientGroup' G H k ≅ QuotientGroup' G H k'
  snrapply Build_GroupIsomorphism'.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
QuotientGroup' G H k <~> QuotientGroup' G H k'
G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
IsSemiGroupPreserving ?f
  1: reflexivity.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
IsSemiGroupPreserving 1%equiv
  intro x.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
x: QuotientGroup' G H k
forall y : QuotientGroup' G H k,
1%equiv (x * y) = 1%equiv x * 1%equiv y
  srapply Quotient_ind_hprop; intro y; revert x.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
y: G
forall x : QuotientGroup' G H k,
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := H;
              normalsubgroup_isnormal := k
            |}) =>
 1%equiv (x * q) = 1%equiv x * 1%equiv q)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := H;
          normalsubgroup_isnormal := k
        |}) y)
  srapply Quotient_ind_hprop; intro x.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
y, x: G
(fun
   q : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := H;
              normalsubgroup_isnormal := k
            |}) =>
 (fun
    q0 : Quotient
           (in_cosetL
              {|
                normalsubgroup_subgroup := H;
                normalsubgroup_isnormal := k
              |}) =>
  1%equiv (q * q0) = 1%equiv q * 1%equiv q0)
   (class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := H;
           normalsubgroup_isnormal := k
         |}) y))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := H;
          normalsubgroup_isnormal := k
        |}) x)
  reflexivity.
Defined.

(** The universal mapping property for groups *)
Theorem equiv_grp_quotient_ump {F : Funext} {G : Group} (N : NormalSubgroup G) (H : Group)
  : {f : G $-> H & forall (n : G), N n -> f n = mon_unit}
    <~> (G / N $-> H).F: Funext
G: Group
N: NormalSubgroup G
H: Group
{f : G $-> H & forall n : G, N n -> f n = mon_unit} <~>
(G / N $-> H)
Proof.F: Funext
G: Group
N: NormalSubgroup G
H: Group
{f : G $-> H & forall n : G, N n -> f n = mon_unit} <~>
(G / N $-> H)
  srapply equiv_adjointify.F: Funext
G: Group
N: NormalSubgroup G
H: Group
{f : G $-> H & forall n : G, N n -> f n = mon_unit} ->
G / N $-> H
F: Funext
G: Group
N: NormalSubgroup G
H: Group
(G / N $-> H) ->
{f : G $-> H & forall n : G, N n -> f n = mon_unit}
F: Funext
G: Group
N: NormalSubgroup G
H: Group
?f o ?g == idmap
F: Funext
G: Group
N: NormalSubgroup G
H: Group
?g o ?f == idmap
  -F: Funext
G: Group
N: NormalSubgroup G
H: Group
{f : G $-> H & forall n : G, N n -> f n = mon_unit} ->
G / N $-> H intros [f p].F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G $-> H
p: forall n : G, N n -> f n = mon_unit
G / N $-> H
    exact (grp_quotient_rec _ _ f p).
  -F: Funext
G: Group
N: NormalSubgroup G
H: Group
(G / N $-> H) ->
{f : G $-> H & forall n : G, N n -> f n = mon_unit} intro f.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
{f : G $-> H & forall n : G, N n -> f n = mon_unit}
    exists (f $o grp_quotient_map).F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
forall n : G,
N n -> (f $o grp_quotient_map) n = mon_unit
    intros n h; cbn.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
n: G
h: N n
f (class_of (fun x y : G => N (- x * y)) n) = mon_unit
    refine (_ @ grp_homo_unit f).F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
n: G
h: N n
f (class_of (fun x y : G => N (- x * y)) n) =
f mon_unit
    apply ap.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
n: G
h: N n
class_of (fun x y : G => N (- x * y)) n = mon_unit
    apply qglue; cbn.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
n: G
h: N n
N (- n * mon_unit)
    rewrite right_identity;
      by apply issubgroup_in_inv.
  -F: Funext
G: Group
N: NormalSubgroup G
H: Group
(fun
   X : {f : G $-> H &
       forall n : G, N n -> f n = mon_unit} =>
 (fun (f : G $-> H)
    (p : forall n : G, N n -> f n = mon_unit) =>
  grp_quotient_rec G N f p) X.1 X.2)
o (fun f : G / N $-> H =>
   (f $o grp_quotient_map;
   fun (n : G) (h : N n) =>
   ap f
     (qglue
        (internal_paths_rew_r (fun g : G => N g)
           (issubgroup_in_inv n h)
           (right_identity (- n))
         :
         in_cosetL N n mon_unit)) @ grp_homo_unit f
   :
   (f $o grp_quotient_map) n = mon_unit)) == idmap intros f.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
grp_quotient_rec G N (f $o grp_quotient_map)
  (fun (n : G) (h : N n) =>
   ap f
     (qglue
        (internal_paths_rew_r (fun g : G => N g)
           (issubgroup_in_inv n h)
           (right_identity (- n)))) @ grp_homo_unit f) =
f
    rapply equiv_path_grouphomomorphism.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
grp_quotient_rec G N (f $o grp_quotient_map)
  (fun (n : G) (h : N n) =>
   ap f
     (qglue
        (internal_paths_rew_r (fun g : G => N g)
           (issubgroup_in_inv n h)
           (right_identity (- n)))) @ grp_homo_unit f) ==
f
      by srapply Quotient_ind_hprop.
  -F: Funext
G: Group
N: NormalSubgroup G
H: Group
(fun f : G / N $-> H =>
 (f $o grp_quotient_map;
 fun (n : G) (h : N n) =>
 ap f
   (qglue
      (internal_paths_rew_r (fun g : G => N g)
         (issubgroup_in_inv n h)
         (right_identity (- n))
       :
       in_cosetL N n mon_unit)) @ grp_homo_unit f
 :
 (f $o grp_quotient_map) n = mon_unit))
o (fun
     X : {f : G $-> H &
         forall n : G, N n -> f n = mon_unit} =>
   (fun (f : G $-> H)
      (p : forall n : G, N n -> f n = mon_unit) =>
    grp_quotient_rec G N f p) X.1 X.2) == idmap intros [f p].F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G $-> H
p: forall n : G, N n -> f n = mon_unit
(grp_quotient_rec G N f p $o grp_quotient_map;
fun (n : G) (h : N n) =>
ap (grp_quotient_rec G N f p)
  (qglue
     (internal_paths_rew_r (fun g : G => N g)
        (issubgroup_in_inv n h) (right_identity (- n)))) @
grp_homo_unit (grp_quotient_rec G N f p)) = (f; p)
    srapply path_sigma_hprop; simpl.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G $-> H
p: forall n : G, N n -> f n = mon_unit
grp_homo_compose (grp_quotient_rec G N f p)
  grp_quotient_map = f
    exact (grp_quotient_rec_beta N H f p).
Defined.

Section FirstIso.

  Context `{Funext} {A B : Group} (phi : A $-> B).

  (** First we define a map from the quotient by the kernel of phi into the image of phi *)
  Definition grp_image_quotient
    : A / grp_kernel phi $-> grp_image phi.H: Funext
A, B: Group
phi: A $-> B
A / grp_kernel phi $-> grp_image phi
  Proof.H: Funext
A, B: Group
phi: A $-> B
A / grp_kernel phi $-> grp_image phi
    srapply grp_quotient_rec.H: Funext
A, B: Group
phi: A $-> B
A $-> grp_image phi
H: Funext
A, B: Group
phi: A $-> B
forall n : A, grp_kernel phi n -> ?f n = mon_unit
    +H: Funext
A, B: Group
phi: A $-> B
A $-> grp_image phi srapply grp_image_in.
    +H: Funext
A, B: Group
phi: A $-> B
forall n : A,
grp_kernel phi n -> grp_image_in phi n = mon_unit intros n x.H: Funext
A, B: Group
phi: A $-> B
n: A
x: grp_kernel phi n
grp_image_in phi n = mon_unit
      by apply path_sigma_hprop.
  Defined.

  (** The underlying map of this homomorphism is an equivalence *)
  Global Instance isequiv_grp_image_quotient
    : IsEquiv grp_image_quotient.H: Funext
A, B: Group
phi: A $-> B
IsEquiv grp_image_quotient
  Proof.H: Funext
A, B: Group
phi: A $-> B
IsEquiv grp_image_quotient
    snrapply isequiv_surj_emb.H: Funext
A, B: Group
phi: A $-> B
IsConnMap (Tr (-1)) grp_image_quotient
H: Funext
A, B: Group
phi: A $-> B
IsEmbedding grp_image_quotient
    1: srapply cancelR_conn_map.H: Funext
A, B: Group
phi: A $-> B
IsEmbedding grp_image_quotient
    srapply isembedding_isinj_hset.H: Funext
A, B: Group
phi: A $-> B
isinj grp_image_quotient
    refine (Quotient_ind_hprop _ _ _); intro x.H: Funext
A, B: Group
phi: A $-> B
x: A
forall x1 : A / grp_kernel phi,
grp_image_quotient
  (class_of (in_cosetL (grp_kernel phi)) x) =
grp_image_quotient x1 ->
class_of (in_cosetL (grp_kernel phi)) x = x1
    refine (Quotient_ind_hprop _ _ _); intro y.H: Funext
A, B: Group
phi: A $-> B
x, y: A
grp_image_quotient
  (class_of (in_cosetL (grp_kernel phi)) x) =
grp_image_quotient
  (class_of (in_cosetL (grp_kernel phi)) y) ->
class_of (in_cosetL (grp_kernel phi)) x =
class_of (in_cosetL (grp_kernel phi)) y
    intros h; simpl in h.H: Funext
A, B: Group
phi: A $-> B
x, y: A
h: (phi x; tr (x; 1%path)) = (phi y; tr (y; 1%path))
class_of (in_cosetL (grp_kernel phi)) x =
class_of (in_cosetL (grp_kernel phi)) y
    apply qglue; cbn.H: Funext
A, B: Group
phi: A $-> B
x, y: A
h: (phi x; tr (x; 1%path)) = (phi y; tr (y; 1%path))
phi (- x * y) = group_unit
    apply (equiv_path_sigma_hprop _ _)^-1%equiv in h; cbn in h.H: Funext
A, B: Group
phi: A $-> B
x, y: A
h: phi x = phi y
phi (- x * y) = group_unit
    cbn.H: Funext
A, B: Group
phi: A $-> B
x, y: A
h: phi x = phi y
phi (- x * y) = group_unit rewrite grp_homo_op, grp_homo_inv, h.H: Funext
A, B: Group
phi: A $-> B
x, y: A
h: phi x = phi y
- phi y * phi y = group_unit
    srapply negate_l.
  Defined.

  (** First isomorphism theorem for groups *)
  Theorem grp_first_iso : A / grp_kernel phi ≅ grp_image phi.H: Funext
A, B: Group
phi: A $-> B
A / grp_kernel phi ≅ grp_image phi
  Proof.H: Funext
A, B: Group
phi: A $-> B
A / grp_kernel phi ≅ grp_image phi
    exact (Build_GroupIsomorphism _ _ grp_image_quotient _).
  Defined.

End FirstIso.

(** Quotient groups are finite. *)
(** Note that we cannot constructively conclude that the normal subgroup [H] must be finite since [G] is, therefore we keep it as an assumption. *)
Global Instance finite_quotientgroup {U : Univalence} (G : Group) (H : NormalSubgroup G)
  (fin_G : Finite G) (fin_H : Finite H)
  : Finite (QuotientGroup G H).U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
Finite (G / H)
Proof.U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
Finite (G / H)
  nrapply finite_quotient.U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
Finite G
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
is_mere_relation G (in_cosetL H)
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
Reflexive (in_cosetL H)
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
Transitive (in_cosetL H)
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
Symmetric (in_cosetL H)
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
forall x y : G, Decidable (in_cosetL H x y)
  1-5: exact _.U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
forall x y : G, Decidable (in_cosetL H x y)
  intros x y.U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
x, y: G
Decidable (in_cosetL H x y)
  pose (dec_H := detachable_finite_subset H).U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
x, y: G
dec_H:= detachable_finite_subset H: forall x : G, Decidable (H x)
Decidable (in_cosetL H x y)
  apply dec_H.
Defined.

Definition grp_kernel_quotient_iso `{Univalence} {G : Group} (N : NormalSubgroup G)
  : GroupIsomorphism N (grp_kernel (@grp_quotient_map G N)).H: Univalence
G: Group
N: NormalSubgroup G
GroupIsomorphism N (grp_kernel grp_quotient_map)
Proof.H: Univalence
G: Group
N: NormalSubgroup G
GroupIsomorphism N (grp_kernel grp_quotient_map)
  srapply Build_GroupIsomorphism.H: Univalence
G: Group
N: NormalSubgroup G
GroupHomomorphism N (grp_kernel grp_quotient_map)
H: Univalence
G: Group
N: NormalSubgroup G
IsEquiv ?grp_iso_homo
  -H: Univalence
G: Group
N: NormalSubgroup G
GroupHomomorphism N (grp_kernel grp_quotient_map) srapply (grp_kernel_corec (subgroup_incl N)).H: Univalence
G: Group
N: NormalSubgroup G
grp_quotient_map $o subgroup_incl N == grp_homo_const
    intro x; cbn.H: Univalence
G: Group
N: NormalSubgroup G
x: N
class_of (fun x y : G => N (- x * y)) x.1 =
congquot_mon_unit
    apply qglue.H: Univalence
G: Group
N: NormalSubgroup G
x: N
N (- x.1 * mon_unit)
    apply issubgroup_in_op.H: Univalence
G: Group
N: NormalSubgroup G
x: N
N (- x.1)
H: Univalence
G: Group
N: NormalSubgroup G
x: N
N mon_unit
    +H: Univalence
G: Group
N: NormalSubgroup G
x: N
N (- x.1) exact (issubgroup_in_inv _ x.2).
    +H: Univalence
G: Group
N: NormalSubgroup G
x: N
N mon_unit exact issubgroup_in_unit.
  -H: Univalence
G: Group
N: NormalSubgroup G
IsEquiv
  (grp_kernel_corec (subgroup_incl N)
     ((fun x : N =>
       qglue
         (issubgroup_in_op (- x.1) mon_unit
            (issubgroup_in_inv x.1 x.2)
            issubgroup_in_unit)
       :
       (grp_quotient_map $o subgroup_incl N) x =
       grp_homo_const x)
      :
      grp_quotient_map $o subgroup_incl N ==
      grp_homo_const)) apply isequiv_surj_emb.H: Univalence
G: Group
N: NormalSubgroup G
IsConnMap (Tr (-1))
  (grp_kernel_corec (subgroup_incl N)
     (fun x : N =>
      qglue
        (issubgroup_in_op (- x.1) mon_unit
           (issubgroup_in_inv x.1 x.2)
           issubgroup_in_unit)))
H: Univalence
G: Group
N: NormalSubgroup G
IsEmbedding
  (grp_kernel_corec (subgroup_incl N)
     (fun x : N =>
      qglue
        (issubgroup_in_op (- x.1) mon_unit
           (issubgroup_in_inv x.1 x.2)
           issubgroup_in_unit)))
    2: apply (cancelL_isembedding (g:=pr1)).H: Univalence
G: Group
N: NormalSubgroup G
IsConnMap (Tr (-1))
  (grp_kernel_corec (subgroup_incl N)
     (fun x : N =>
      qglue
        (issubgroup_in_op (- x.1) mon_unit
           (issubgroup_in_inv x.1 x.2)
           issubgroup_in_unit)))
    intros [g p].H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
IsConnected (Tr (-1))
  (hfiber
     (grp_kernel_corec (subgroup_incl N)
        (fun x : N =>
         qglue
           (issubgroup_in_op (- x.1) mon_unit
              (issubgroup_in_inv x.1 x.2)
              issubgroup_in_unit))) (g; p))
    rapply contr_inhabited_hprop.H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
Tr (-1)
  (hfiber
     (grp_kernel_corec (subgroup_incl N)
        (fun x : N =>
         qglue
           (issubgroup_in_op (- x.1) mon_unit
              (issubgroup_in_inv x.1 x.2)
              issubgroup_in_unit))) (g; p))
    srefine (tr ((g; _); _)).H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
N g
H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
(fun x : N =>
 grp_kernel_corec (subgroup_incl N)
   (fun x0 : N =>
    qglue
      (issubgroup_in_op (- x0.1) mon_unit
         (issubgroup_in_inv x0.1 x0.2)
         issubgroup_in_unit)) x = (g; p)) (g; ?proj2)
    +H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
N g rewrite <- grp_unit_l, <- negate_mon_unit.H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
N (- mon_unit * g)
      apply (related_quotient_paths (fun x y => N (-x * y))).H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
class_of (fun x y : G => N (- x * y)) mon_unit =
class_of (fun x y : G => N (- x * y)) g
      exact p^.
    +H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
(fun x : N =>
 grp_kernel_corec (subgroup_incl N)
   (fun x0 : N =>
    qglue
      (issubgroup_in_op (- x0.1) mon_unit
         (issubgroup_in_inv x0.1 x0.2)
         issubgroup_in_unit)) x = (g; p))
  (g;
  internal_paths_rew N
    (internal_paths_rew (fun g0 : G => N (g0 * g))
       (related_quotient_paths
          (fun x y : G => N (- x * y)) mon_unit g p^)
       negate_mon_unit) (grp_unit_l g)) srapply path_sigma_hprop.H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
(grp_kernel_corec (subgroup_incl N)
   (fun x : N =>
    qglue
      (issubgroup_in_op (- x.1) mon_unit
         (issubgroup_in_inv x.1 x.2)
         issubgroup_in_unit))
   (g;
   internal_paths_rew N
     (internal_paths_rew (fun g0 : G => N (g0 * g))
        (related_quotient_paths
           (fun x y : G => N (- x * y)) mon_unit g p^)
        negate_mon_unit) (grp_unit_l g))).1 = (g; p).1
      reflexivity.
Defined.