HoTT.Algebra.Groups.QuotientGroup.v.alectryon.json

From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
Require Import Truncations.Core.
Require Import Algebra.Congruence.
Require Import Algebra.Groups.Group.
Require Import Algebra.Groups.Subgroup.
Require Export Colimits.Quotient.
Require Import HSet.
Require Import Spaces.Finite.Finite.
From HoTT.WildCat Require Import Core Equiv.
Require Import Modalities.Modality.

(** * Quotient groups *)

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

(** ** Congruence quotients *)

Section GroupCongruenceQuotient.

  (** A congruence on a group is a relation satisfying [R x x' -> R y y' -> R (x * y) (x' * y')].  Because we also require that [R] is reflexive, we also know that [R y y' -> R (x * y) (x * y')] for any [x], and similarly for multiplication on the right by [x].  We don't need to assume that [R] is symmetric or transitive. *)
  Context {G : Group} {R : Relation G} `{!IsCongruence R, !Reflexive R}.

  (** The type underlying the quotient group is [Quotient R]. *)
  Definition CongruenceQuotient := G / R.

  #[export] Instance congquot_sgop : SgOp CongruenceQuotient.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
SgOp CongruenceQuotient
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
SgOp CongruenceQuotient
    srapply Quotient_rec2.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
G -> G -> CongruenceQuotient
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
forall a a' b : G, R a a' -> ?dclass a b = ?dclass a' b
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
forall a b b' : G, R b b' -> ?dclass a b = ?dclass a b'
    -G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
G -> G -> CongruenceQuotient intros x y.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
CongruenceQuotient
      exact (class_of _ (x * y)).
    -G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
forall a a' b : G,
R a a' ->
(fun x y : G => class_of R (x * y)) a b =
(fun x y : G => class_of R (x * y)) a' b intros x x' y p.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, x', y: G
p: R x x'
(fun x0 y0 : G => class_of R (x0 * y0)) x y =
(fun x0 y0 : G => class_of R (x0 * y0)) x' y apply qglue.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, x', y: G
p: R x x'
R (x * y) (x' * y) by apply iscong.
    -G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
forall a b b' : G,
R b b' ->
(fun x y : G => class_of R (x * y)) a b =
(fun x y : G => class_of R (x * y)) a b' intros x y y' q.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y, y': G
q: R y y'
(fun x0 y0 : G => class_of R (x0 * y0)) x y =
(fun x0 y0 : G => class_of R (x0 * y0)) x y' apply qglue.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y, y': G
q: R y y'
R (x * y) (x * y') by apply iscong.
  Defined.

  #[export] Instance congquot_mon_unit : MonUnit CongruenceQuotient.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
MonUnit CongruenceQuotient
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
MonUnit CongruenceQuotient
    apply class_of, mon_unit.
  Defined.

  #[export] Instance congquot_inverse : Inverse CongruenceQuotient.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Inverse CongruenceQuotient
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Inverse CongruenceQuotient
    srapply Quotient_rec.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
G -> CongruenceQuotient
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
forall a b : G, R a b -> ?pclass a = ?pclass b
    1: exact (class_of R o (^)).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
forall a b : G, R a b -> (class_of R o inv) a = (class_of R o inv) b
    intros x y p; cbn beta.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R x^ = class_of R y^
    transitivity (class_of R (y^ * (y * x^))).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R x^ = class_of R (y^ * (y * x^))
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * (y * x^)) = class_of R y^
    -G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R x^ = class_of R (y^ * (y * x^)) rewrite grp_assoc.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R x^ = class_of R (y^ * y * x^)
      rewrite grp_inv_l.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R x^ = class_of R (1 * x^)
      rewrite grp_unit_l.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R x^ = class_of R x^
      reflexivity.
    -G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * (y * x^)) = class_of R y^ transitivity (class_of R (y^ * (x * x^))).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * (y * x^)) = class_of R (y^ * (x * x^))
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * (x * x^)) = class_of R y^
      +G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * (y * x^)) = class_of R (y^ * (x * x^)) symmetry; apply qglue; repeat apply iscong.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
R y^ y^
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
R x y
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
R x^ x^
        1,3: reflexivity.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
R x y
        exact p.
      +G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * (x * x^)) = class_of R y^ rewrite grp_inv_r.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * 1) = class_of R y^
        rewrite grp_unit_r.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R y^ = class_of R y^
        reflexivity.
  Defined.

  #[export] Instance congquot_sgop_associative : Associative congquot_sgop.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Associative congquot_sgop
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Associative congquot_sgop
    srapply Quotient_ind3_hprop; intros x y z.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y, z: G
(fun x0 y0 z0 : G / R =>
 congquot_sgop x0 (congquot_sgop y0 z0) =
 congquot_sgop (congquot_sgop x0 y0) z0) (class_of R x) 
  (class_of R y) (class_of R z)
    snapply (ap (class_of R)).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y, z: G
x * (y * z) = x * y * z
    rapply associativity.
  Defined.
  Global Opaque congquot_sgop_associative.

  #[export] Instance issemigroup_congquot : IsSemiGroup CongruenceQuotient := {}.

  #[export] Instance congquot_leftidentity : LeftIdentity (.*.) mon_unit.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
LeftIdentity sg_op 1
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
LeftIdentity sg_op 1
    srapply Quotient_ind_hprop; intro x.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
(fun x0 : G / R => 1 * x0 = x0) (class_of R x)
    snapply (ap (class_of R)).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
1 * x = x
    rapply left_identity.
  Defined.
  Global Opaque congquot_leftidentity.

  #[export] Instance congquot_rightidentity : RightIdentity (.*.) mon_unit.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
RightIdentity sg_op 1
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
RightIdentity sg_op 1
    srapply Quotient_ind_hprop; intro x.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
(fun x0 : G / R => x0 * 1 = x0) (class_of R x)
    snapply (ap (class_of R)).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
x * 1 = x
    rapply right_identity.
  Defined.
  Global Opaque congquot_rightidentity.

  #[export] Instance ismonoid_quotientgroup : IsMonoid CongruenceQuotient := {}.

  #[export] Instance quotientgroup_leftinverse : LeftInverse (.*.) (^) mon_unit.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
LeftInverse sg_op inv 1
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
LeftInverse sg_op inv 1
    srapply Quotient_ind_hprop; intro x; cbn beta.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
(class_of R x)^ * class_of R x = 1
    snapply (ap (class_of R)).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
x^ * x = 1
    rapply left_inverse.
  Defined.
  Global Opaque quotientgroup_leftinverse.

  #[export] Instance quotientgroup_rightinverse : RightInverse (.*.) (^) mon_unit.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
RightInverse sg_op inv 1
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
RightInverse sg_op inv 1
    srapply Quotient_ind_hprop; intro x; cbn beta.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
class_of R x * (class_of R x)^ = 1
    snapply (ap (class_of R)).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
x * x^ = 1
    rapply right_inverse.
  Defined.
  Global Opaque quotientgroup_rightinverse.

  #[export] Instance isgroup_quotientgroup : IsGroup CongruenceQuotient := {}.

End GroupCongruenceQuotient.

(** ** Sets of cosets *)

Section Cosets.

  Context (G : Group) (H : Subgroup G).

  Definition LeftCoset := G / in_cosetL H.

  (** TODO: Way too many universes, needs fixing *)
  (** The set of left cosets of a finite subgroup of a finite group is finite. *)
  #[export] Instance finite_leftcoset `{Univalence, Finite G, Finite H}
    : Finite LeftCoset.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite LeftCoset
  Proof.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite LeftCoset
    napply finite_quotient.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite G
G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
is_mere_relation G (in_cosetL H)
G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Reflexive (in_cosetL H)
G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Transitive (in_cosetL H)
G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Symmetric (in_cosetL H)
G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
forall x y : G, Decidable (in_cosetL H x y)
    1-5: exact _.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
forall x y : G, Decidable (in_cosetL H x y)
    intros x y.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
x, y: G
Decidable (in_cosetL H x y)
    apply (detachable_finite_subset H).
  Defined.

  (** The index of a subgroup is the number of cosets of the subgroup. *)
  Definition subgroup_index `{Univalence, Finite G, Finite H} : nat
    := fcard LeftCoset.

  Definition RightCoset := G / in_cosetR H.

  (** The set of left cosets is equivalent to the set of right coset. *)
  Definition equiv_leftcoset_rightcoset
    : LeftCoset <~> RightCoset.G: Group
H: Subgroup G
LeftCoset <~> RightCoset
  Proof.G: Group
H: Subgroup G
LeftCoset <~> RightCoset
    snapply equiv_quotient_functor.G: Group
H: Subgroup G
G -> G
G: Group
H: Subgroup G
IsEquiv ?f
G: Group
H: Subgroup G
forall a b : G, in_cosetL H a b <-> in_cosetR H (?f a) (?f b)
    -G: Group
H: Subgroup G
G -> G exact inv.
    -G: Group
H: Subgroup G
IsEquiv inv exact _.
    -G: Group
H: Subgroup G
forall a b : G, in_cosetL H a b <-> in_cosetR H a^ b^ intros x y; simpl.G: Group
H: Subgroup G
x, y: G
H (x^ * y) <-> H (x^ * (y^)^)
      by rewrite grp_inv_inv.
  Defined.

  (** The set of right cosets of a finite subgroup of a finite group is finite since it is equivalent to the set of left cosets. *)
  #[export] Instance finite_rightcoset `{Univalence, Finite G, Finite H}
    : Finite RightCoset.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite RightCoset
  Proof.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite RightCoset
    napply finite_equiv'.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
?Goal <~> RightCoset
G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite ?Goal
    1: exact equiv_leftcoset_rightcoset.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite LeftCoset
    exact _.
  Defined.

End Cosets.

(** ** Quotient groups *)

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

Section QuotientGroup.

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

  #[export] 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.

  #[export] 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 (LeftCoset G N) _ _ _ _.

  Definition grp_quotient_map : G $-> QuotientGroup.G: Group
N: NormalSubgroup G
G $-> QuotientGroup
  Proof.G: Group
N: NormalSubgroup G
G $-> QuotientGroup
    snapply Build_GroupHomomorphism.G: Group
N: NormalSubgroup G
G -> QuotientGroup
G: Group
N: NormalSubgroup G
IsSemiGroupPreserving ?grp_homo_map
    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 = 1
QuotientGroup $-> A
  Proof.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
QuotientGroup $-> A
    snapply Build_GroupHomomorphism.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
QuotientGroup -> A
G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
IsSemiGroupPreserving ?grp_homo_map
    -G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
QuotientGroup -> A srapply Quotient_rec.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
G -> A
G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
forall a b : G, in_cosetL N a b -> ?pclass a = ?pclass b
      +G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
G -> A exact f.
      +G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
forall a b : G, in_cosetL N a b -> f a = f b cbn; intros x y n.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n0 : G, N n0 -> f n0 = 1
x, y: G
n: N (x^ * y)
f x = f y
        apply grp_moveR_M1.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n0 : G, N n0 -> f n0 = 1
x, y: G
n: N (x^ * y)
1 = (f x)^ * f y
        rhs_V napply (ap (.* f y) (grp_homo_inv _ _)).G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n0 : G, N n0 -> f n0 = 1
x, y: G
n: N (x^ * y)
1 = f x^ * f y
        rhs_V napply grp_homo_op.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n0 : G, N n0 -> f n0 = 1
x, y: G
n: N (x^ * y)
1 = f (x^ * y)
        symmetry; apply h; assumption.
    -G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
IsSemiGroupPreserving
  (Quotient_rec (in_cosetL N) A f
     ((fun (x y : G) (n : N (x^ * y)) =>
       let X := equiv_fun grp_moveR_M1 in
       X
         (((h (inv x * y) n)^ @ grp_homo_op f (inv x) y) @
          ap (fun y0 : A => y0 * f y) (grp_homo_inv f x)))
      :
      forall a b : G, in_cosetL N a b -> f a = f b)) intro x.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
x: QuotientGroup
forall y : QuotientGroup,
Quotient_rec (in_cosetL N) A f
  (fun (x0 y0 : G) (n : N (x0^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y0) n)^ @ grp_homo_op f (inv x0) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x0)))
  (x * y) =
Quotient_rec (in_cosetL N) A f
  (fun (x0 y0 : G) (n : N (x0^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y0) n)^ @ grp_homo_op f (inv x0) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x0)))
  x *
Quotient_rec (in_cosetL N) A f
  (fun (x0 y0 : G) (n : N (x0^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y0) n)^ @ grp_homo_op f (inv x0) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x0)))
  y
      refine (Quotient_ind_hprop _ _ _).G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
x: QuotientGroup
forall a : G,
Quotient_rec (in_cosetL N) A f
  (fun (x0 y : G) (n : N (x0^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y) n)^ @ grp_homo_op f (inv x0) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x0)))
  (x * class_of (in_cosetL N) a) =
Quotient_rec (in_cosetL N) A f
  (fun (x0 y : G) (n : N (x0^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y) n)^ @ grp_homo_op f (inv x0) y) @
      ap (fun y0 : A => y0 * f 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_moveR_M1 in
   X
     (((h (inv x0 * y) n)^ @ grp_homo_op f (inv x0) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x0)))
  (class_of (in_cosetL N) a)
      intro y.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
x: QuotientGroup
y: G
Quotient_rec (in_cosetL N) A f
  (fun (x0 y0 : G) (n : N (x0^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y0) n)^ @ grp_homo_op f (inv x0) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x0)))
  (x * class_of (in_cosetL N) y) =
Quotient_rec (in_cosetL N) A f
  (fun (x0 y0 : G) (n : N (x0^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y0) n)^ @ grp_homo_op f (inv x0) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x0)))
  x *
Quotient_rec (in_cosetL N) A f
  (fun (x0 y0 : G) (n : N (x0^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y0) n)^ @ grp_homo_op f (inv x0) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x0)))
  (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 = 1
y: G
forall x : QuotientGroup,
Quotient_rec (in_cosetL N) A f
  (fun (x0 y0 : G) (n : N (x0^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y0) n)^ @ grp_homo_op f (inv x0) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x0)))
  (x * class_of (in_cosetL N) y) =
Quotient_rec (in_cosetL N) A f
  (fun (x0 y0 : G) (n : N (x0^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y0) n)^ @ grp_homo_op f (inv x0) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x0)))
  x *
Quotient_rec (in_cosetL N) A f
  (fun (x0 y0 : G) (n : N (x0^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y0) n)^ @ grp_homo_op f (inv x0) y0) @
      ap (fun y1 : A => y1 * f y0) (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 = 1
y: G
forall a : G,
Quotient_rec (in_cosetL N) A f
  (fun (x y0 : G) (n : N (x^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y0) n)^ @ grp_homo_op f (inv x) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x)))
  (class_of (in_cosetL N) a * class_of (in_cosetL N) y) =
Quotient_rec (in_cosetL N) A f
  (fun (x y0 : G) (n : N (x^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y0) n)^ @ grp_homo_op f (inv x) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x)))
  (class_of (in_cosetL N) a) *
Quotient_rec (in_cosetL N) A f
  (fun (x y0 : G) (n : N (x^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y0) n)^ @ grp_homo_op f (inv x) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x)))
  (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 = 1
y, x: G
f (x * y) = f x * f y
      apply grp_homo_op.
  Defined.

  Definition grp_quotient_ind_hprop (P : QuotientGroup -> Type)
    `{forall x, IsHProp (P x)}
    (H1 : forall x, P (grp_quotient_map x))
    : forall x, P x.G: Group
N: NormalSubgroup G
P: QuotientGroup -> Type
H: forall x : QuotientGroup, IsHProp (P x)
H1: forall x : G, P (grp_quotient_map x)
forall x : QuotientGroup, P x
  Proof.G: Group
N: NormalSubgroup G
P: QuotientGroup -> Type
H: forall x : QuotientGroup, IsHProp (P x)
H1: forall x : G, P (grp_quotient_map x)
forall x : QuotientGroup, P x
    srapply Quotient_ind_hprop.G: Group
N: NormalSubgroup G
P: QuotientGroup -> Type
H: forall x : QuotientGroup, IsHProp (P x)
H1: forall x : G, P (grp_quotient_map x)
forall a : G, P (class_of (in_cosetL N) a)
    exact H1.
  Defined.

End QuotientGroup.

Arguments QuotientGroup G N : simpl never.
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 = 1
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 = 1
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 irrelevant up to equivalence. It 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'
  snapply 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
   x0 : Quotient
          (in_cosetL
             {| normalsubgroup_subgroup := H; normalsubgroup_isnormal := k |}) =>
 1%equiv (x * x0) = 1%equiv x * 1%equiv x0)
  (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
   x0 : Quotient
          (in_cosetL
             {| normalsubgroup_subgroup := H; normalsubgroup_isnormal := k |}) =>
 (fun
    x1 : Quotient
           (in_cosetL
              {|
                normalsubgroup_subgroup := H; normalsubgroup_isnormal := k
              |}) =>
  1%equiv (x0 * x1) = 1%equiv x0 * 1%equiv x1)
   (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 quotient map is trivial on the normal subgroup. *)
Definition grp_quotient_map_trivial {G : Group} (N : NormalSubgroup G)
  (n : G) (inN : N n)
  : grp_quotient_map (N:=N) n = 1.G: Group
N: NormalSubgroup G
n: G
inN: N n
grp_quotient_map n = 1
Proof.G: Group
N: NormalSubgroup G
n: G
inN: N n
grp_quotient_map n = 1
  apply qglue; cbn.G: Group
N: NormalSubgroup G
n: G
inN: N n
N (n^ * 1)
  rewrite right_identity.G: Group
N: NormalSubgroup G
n: G
inN: N n
N n^
  by apply issubgroup_in_inv.
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 = 1} <~> (G / N $-> H)
Proof.F: Funext
G: Group
N: NormalSubgroup G
H: Group
{f : G $-> H & forall n : G, N n -> f n = 1} <~> (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 = 1} -> 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 = 1}
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 = 1} -> 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 = 1
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 = 1} intro f.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
{f0 : G $-> H & forall n : G, N n -> f0 n = 1}
    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 = 1
    intros n h.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
n: G
h: N n
(f $o grp_quotient_map) n = 1
    rhs_V napply (grp_homo_unit f).F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
n: G
h: N n
(f $o grp_quotient_map) n = f 1
    apply (ap f).F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
n: G
h: N n
grp_quotient_map n = 1
    by apply grp_quotient_map_trivial.
  -F: Funext
G: Group
N: NormalSubgroup G
H: Group
(fun X : {f : G $-> H & forall n : G, N n -> f n = 1} =>
 (fun (f : G $-> H) (p : forall n : G, N n -> f n = 1) =>
  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 (grp_quotient_map_trivial N n h) @ grp_homo_unit f)) ==
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 (grp_quotient_map_trivial N n h) @ 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 (grp_quotient_map_trivial N n h) @ 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 (grp_quotient_map_trivial N n h) @ grp_homo_unit f))
o (fun X : {f : G $-> H & forall n : G, N n -> f n = 1} =>
   (fun (f : G $-> H) (p : forall n : G, N n -> f n = 1) =>
    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 = 1
(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) (grp_quotient_map_trivial N n h) @
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 = 1
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 = 1
    +H: Funext
A, B: Group
phi: A $-> B
A $-> grp_image phi srapply grp_homo_image_in.
    +H: Funext
A, B: Group
phi: A $-> B
forall n : A, grp_kernel phi n -> grp_homo_image_in phi n = 1 intros n x.H: Funext
A, B: Group
phi: A $-> B
n: A
x: grp_kernel phi n
grp_homo_image_in phi n = 1
      by apply path_sigma_hprop.
  Defined.

  (** The underlying map of this homomorphism is an equivalence *)
  #[export] 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
    snapply 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
IsInjective grp_image_quotient
    srapply Quotient_ind2_hprop.H: Funext
A, B: Group
phi: A $-> B
forall a b : A,
(fun x y : Quotient (in_cosetL (grp_kernel phi)) =>
 grp_image_quotient x = grp_image_quotient y -> x = y)
  (class_of (in_cosetL (grp_kernel phi)) a)
  (class_of (in_cosetL (grp_kernel phi)) b)
    intros x y h; simpl in h.H: Funext
A, B: Group
phi: A $-> B
x, y: A
h: (phi x; grp_image_in phi x) = (phi y; grp_image_in phi y)
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; grp_image_in phi x) = (phi y; grp_image_in phi y)
phi (x^ * y) = 1
    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) = 1
    cbn.H: Funext
A, B: Group
phi: A $-> B
x, y: A
h: phi x = phi y
phi (x^ * y) = 1 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 = 1
    apply grp_inv_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. *)
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)
  napply 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 x0 : G, Decidable (H x0)
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.H: Univalence
G: Group
N: NormalSubgroup G
x: N
(grp_quotient_map $o subgroup_incl N) x = grp_homo_const x
    apply grp_quotient_map_trivial.H: Univalence
G: Group
N: NormalSubgroup G
x: N
N (subgroup_incl N x)
    exact x.2.
  -H: Univalence
G: Group
N: NormalSubgroup G
IsEquiv
  (grp_kernel_corec (subgroup_incl N)
     ((fun x : N => grp_quotient_map_trivial N (subgroup_incl N x) x.2)
      :
      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 => grp_quotient_map_trivial N (subgroup_incl N x) x.2))
H: Univalence
G: Group
N: NormalSubgroup G
IsEmbedding
  (grp_kernel_corec (subgroup_incl N)
     (fun x : N => grp_quotient_map_trivial N (subgroup_incl N x) x.2))
    2: exact (cancelL_isembedding (g:=pr1)).H: Univalence
G: Group
N: NormalSubgroup G
IsConnMap (Tr (-1))
  (grp_kernel_corec (subgroup_incl N)
     (fun x : N => grp_quotient_map_trivial N (subgroup_incl N x) x.2))
    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 => grp_quotient_map_trivial N (subgroup_incl N x) x.2))
     (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 => grp_quotient_map_trivial N (subgroup_incl N x) x.2))
     (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 => grp_quotient_map_trivial N (subgroup_incl N x0) x0.2) 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, <- inverse_mon_unit.H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
N (1^ * 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)) 1 =
class_of (fun x y : G => N (x^ * y)) g
      exact p^%path.
    +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 => grp_quotient_map_trivial N (subgroup_incl N x0) x0.2) 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)) 1 g p^)
       inverse_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 => grp_quotient_map_trivial N (subgroup_incl N x) x.2)
   (g;
   internal_paths_rew N
     (internal_paths_rew (fun g0 : G => N (g0 * g))
        (related_quotient_paths (fun x y : G => N (x^ * y)) 1 g p^)
        inverse_mon_unit)
     (grp_unit_l g))).1 =
(g; p).1
      reflexivity.
Defined.

(** When the normal subgroup [N] is trivial, the inclusion map [G $-> G / N] is an isomorphism. *)
Instance catie_grp_quotient_map_trivial {G : Group} (N : NormalSubgroup G)
  (triv : IsTrivialGroup N)
  : CatIsEquiv (@grp_quotient_map G N).G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
CatIsEquiv grp_quotient_map
Proof.G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
CatIsEquiv grp_quotient_map
  snapply catie_adjointify.G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
G / N $-> G
G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
grp_quotient_map $o ?g $== Id (G / N)
G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
?g $o grp_quotient_map $== Id G
  -G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
G / N $-> G srapply (grp_quotient_rec _ _ (Id _)).G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
forall n : G, N n -> Id G n = 1
    exact triv.
  -G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
grp_quotient_map $o grp_quotient_rec G N (Id G) triv $== Id (G / N) by srapply grp_quotient_ind_hprop.
  -G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
grp_quotient_rec G N (Id G) triv $o grp_quotient_map $== Id G reflexivity.
Defined.

(** The group quotient by a trivial group is isomorphic to the original group. *)
Definition grp_quotient_trivial (G : Group) (N : NormalSubgroup G)
  (triv : IsTrivialGroup N)
  : G $<~> G / N
  := Build_CatEquiv grp_quotient_map.

(** A quotient by a maximal subgroup is trivial. *)
Instance istrivial_grp_quotient_maximal
  (G : Group) (N : NormalSubgroup G)
  : IsMaximalSubgroup N -> IsTrivialGroup (G / N).G: Group
N: NormalSubgroup G
IsMaximalSubgroup N -> IsTrivialGroup (maximal_subgroup (G / N))
Proof.G: Group
N: NormalSubgroup G
IsMaximalSubgroup N -> IsTrivialGroup (maximal_subgroup (G / N))
  intros max x _; revert x.G: Group
N: NormalSubgroup G
max: IsMaximalSubgroup N
forall x : G / N, trivial_subgroup (G / N) x
  rapply grp_quotient_ind_hprop.G: Group
N: NormalSubgroup G
max: IsMaximalSubgroup N
forall x : G, trivial_subgroup (G / N) (grp_quotient_map x)
  intros x.G: Group
N: NormalSubgroup G
max: IsMaximalSubgroup N
x: G
trivial_subgroup (G / N) (grp_quotient_map x)
  apply qglue, max.
Defined.

(** Conversely, a trivial quotient means the subgroup is maximal.  First a version where we only assume that the quotient map is trivial. *)
Definition ismaximalsubgroup_istrivial_grp_quotient_map `{Univalence}
  (G : Group) (N : NormalSubgroup G)
  (triv : forall x, grp_quotient_map (N:=N) x = 1)
  : IsMaximalSubgroup N.H: Univalence
G: Group
N: NormalSubgroup G
triv: forall x : G, grp_quotient_map x = 1
IsMaximalSubgroup N
Proof.H: Univalence
G: Group
N: NormalSubgroup G
triv: forall x : G, grp_quotient_map x = 1
IsMaximalSubgroup N
  intro x.H: Univalence
G: Group
N: NormalSubgroup G
triv: forall x0 : G, grp_quotient_map x0 = 1
x: G
N x
  specialize (triv x).H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: grp_quotient_map x = 1
N x
  apply related_quotient_paths in triv.H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: in_cosetL N x 1
N x
H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: grp_quotient_map x = 1
is_mere_relation G (in_cosetL N)
H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: grp_quotient_map x = 1
Transitive (in_cosetL N)
H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: grp_quotient_map x = 1
Symmetric (in_cosetL N)
H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: grp_quotient_map x = 1
Reflexive (in_cosetL N)
  2-5: exact _.H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: in_cosetL N x 1
N x
  apply equiv_subgroup_inv.H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: in_cosetL N x 1
N x^
  napply (subgroup_in_op_l _ _ 1 triv) .H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: in_cosetL N x 1
N 1
  apply subgroup_in_unit.
Defined.

Definition ismaximalsubgroup_istrivial_grp_quotient `{Univalence}
  (G : Group) (N : NormalSubgroup G)
  (triv : IsTrivialGroup (G / N))
  : IsMaximalSubgroup N.H: Univalence
G: Group
N: NormalSubgroup G
triv: IsTrivialGroup (maximal_subgroup (G / N))
IsMaximalSubgroup N
Proof.H: Univalence
G: Group
N: NormalSubgroup G
triv: IsTrivialGroup (maximal_subgroup (G / N))
IsMaximalSubgroup N
  apply ismaximalsubgroup_istrivial_grp_quotient_map.H: Univalence
G: Group
N: NormalSubgroup G
triv: IsTrivialGroup (maximal_subgroup (G / N))
forall x : G, grp_quotient_map x = 1
  intro x.H: Univalence
G: Group
N: NormalSubgroup G
triv: IsTrivialGroup (maximal_subgroup (G / N))
x: G
grp_quotient_map x = 1
  exact (triv (grp_quotient_map x) tt).
Defined.