Require Import Basics Types HFiber WildCat.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.Core.
Require Import Algebra.Groups.Group TruncType.

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.

Generalizable Variables G H A B C N f g.

(** * Subgroups *)

(** A subgroup H of a group G is a predicate (i.e. an hProp-valued type family) on G which is closed under the group operations. The group underlying H is given by the total space { g : G & H g }, defined in [subgroup_group] below. *)
Class IsSubgroup {G : Group} (H : G -> Type) := {
  issubgroup_predicate : forall x, IsHProp (H x) ;
  issubgroup_in_unit : H mon_unit ;
  issubgroup_in_op : forall x y, H x -> H y -> H (x * y) ;
  issubgroup_in_inv : forall x, H x -> H (- x) ;
}.

Global Existing Instance issubgroup_predicate.

(** Smart constructor for subgroups.  *)
Definition Build_IsSubgroup' {G : Group}
  (H : G -> Type) `{forall x, IsHProp (H x)}
  (unit : H mon_unit)
  (c : forall x y, H x -> H y -> H (x * -y))
  : IsSubgroup H.
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
IsSubgroup H
Proof.
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
IsSubgroup H
  refine (Build_IsSubgroup G H _ unit _ _).
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
forall x y : G, H x -> H y -> H (x * y)
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
forall x : G, H x -> H (- x)
  -
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
forall x y : G, H x -> H y -> H (x * y) intros x y.
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
x, y: G
H x -> H y -> H (x * y)
    intros hx hy.
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
x, y: G
hx: H x
hy: H y
H (x * y)
    pose (c' := c mon_unit y).
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
x, y: G
hx: H x
hy: H y
c':= c mon_unit y: H mon_unit -> H y -> H (mon_unit * - y)
H (x * y)
    specialize (c' unit).
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
x, y: G
hx: H x
hy: H y
c': H y -> H (mon_unit * - y)
H (x * y)
    specialize (c x (-y)).
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
x, y: G
c: H x -> H (- y) -> H (x * - - y)
hx: H x
hy: H y
c': H y -> H (mon_unit * - y)
H (x * y)
    rewrite (negate_involutive y) in c.
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
x, y: G
c: H x -> H (- y) -> H (x * y)
hx: H x
hy: H y
c': H y -> H (mon_unit * - y)
H (x * y)
    rewrite left_identity in c'.
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
x, y: G
c: H x -> H (- y) -> H (x * y)
hx: H x
hy: H y
c': H y -> H (- y)
H (x * y)
    apply c.
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
x, y: G
c: H x -> H (- y) -> H (x * y)
hx: H x
hy: H y
c': H y -> H (- y)
H x
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
x, y: G
c: H x -> H (- y) -> H (x * y)
hx: H x
hy: H y
c': H y -> H (- y)
H (- y)
    1: assumption.
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
x, y: G
c: H x -> H (- y) -> H (x * y)
hx: H x
hy: H y
c': H y -> H (- y)
H (- y)
    exact (c' hy).
  -
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
forall x : G, H x -> H (- x) intro g.
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
g: G
H g -> H (- g)
    specialize (c _ g unit).
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
g: G
c: H g -> H (mon_unit * - g)
H g -> H (- g)
    rewrite left_identity in c.
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
g: G
c: H g -> H (- g)
H g -> H (- g)
    assumption.
Defined.

(** Additional lemmas about being elements in a subgroup *)
Section IsSubgroupElements.
  Context  {G : Group} {H : G -> Type} `{IsSubgroup G H}.

  Definition issubgroup_in_op_inv (x y : G) : H x -> H y -> H (x * -y).
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H y -> H (x * - y)
  Proof.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H y -> H (x * - y)
    intros p q.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H (x * - y)
    apply issubgroup_in_op.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H x
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H (- y)
    1: assumption.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H (- y)
    by apply issubgroup_in_inv.
  Defined.

  Definition issubgroup_in_inv' (x : G) : H (- x) -> H x.
G: Group
H: G -> Type
H0: IsSubgroup H
x: G
H (- x) -> H x
  Proof.
G: Group
H: G -> Type
H0: IsSubgroup H
x: G
H (- x) -> H x
    intros p; rewrite <- (negate_involutive x); revert p.
G: Group
H: G -> Type
H0: IsSubgroup H
x: G
H (- x) -> H (- - x)
    apply issubgroup_in_inv.
  Defined.

  Definition issubgroup_in_inv_op (x y : G) : H x -> H y -> H (-x * y).
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H y -> H (- x * y)
  Proof.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H y -> H (- x * y)
    intros p q.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H (- x * y)
    rewrite <- (negate_involutive y).
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H (- x * - - y)
    apply issubgroup_in_op_inv.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H (- x)
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H (- y)
    1,2: by apply issubgroup_in_inv.
  Defined.

  Definition issubgroup_in_op_l (x y : G) : H (x * y) -> H y -> H x.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H y -> H x
  Proof.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H y -> H x
    intros p q.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H (x * y)
q: H y
H x
    rewrite <- (grp_unit_r x).
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H (x * y)
q: H y
H (x * mon_unit)
    revert p q.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H y -> H (x * mon_unit)
    rewrite <- (grp_inv_r y).
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H y -> H (x * (y * - y))
    rewrite grp_assoc.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H y -> H (x * y * - y)
    apply issubgroup_in_op_inv.
  Defined.

  Definition issubgroup_in_op_r (x y : G) : H (x * y) -> H x -> H y.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H x -> H y
  Proof.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H x -> H y
    intros p q.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H (x * y)
q: H x
H y
    rewrite <- (grp_unit_l y).
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H (x * y)
q: H x
H (mon_unit * y)
    revert q p.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H (x * y) -> H (mon_unit * y)
    rewrite <- (grp_inv_l x).
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H (x * y) -> H (- x * x * y)
    rewrite <- grp_assoc.
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H (x * y) -> H (- x * (x * y))
    apply issubgroup_in_inv_op.
  Defined.

End IsSubgroupElements.

Definition issig_issubgroup {G : Group} (H : G -> Type) : _ <~> IsSubgroup H
  := ltac:(issig).

(** Given a predicate H on a group G, being a subgroup is a property. *)
Global Instance ishprop_issubgroup `{F : Funext} {G : Group} {H : G -> Type}
  : IsHProp (IsSubgroup H).
F: Funext
G: Group
H: G -> Type
IsHProp (IsSubgroup H)
Proof.
F: Funext
G: Group
H: G -> Type
IsHProp (IsSubgroup H)
  exact (istrunc_equiv_istrunc _ (issig_issubgroup H)).
Defined.

(** The type (set) of subgroups of a group G. *)
Record Subgroup (G : Group) := {
  subgroup_pred : G -> Type ;
  subgroup_issubgroup : IsSubgroup subgroup_pred ;
}.

Coercion subgroup_pred : Subgroup >-> Funclass.
Global Existing Instance subgroup_issubgroup.

Definition Build_Subgroup' {G : Group}
  (H : G -> Type) `{forall x, IsHProp (H x)}
  (unit : H mon_unit)
  (c : forall x y, H x -> H y -> H (x * -y))
  : Subgroup G.
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
Subgroup G
Proof.
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
Subgroup G
  refine (Build_Subgroup G H _).
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H mon_unit
c: forall x y : G, H x -> H y -> H (x * - y)
IsSubgroup H
  rapply Build_IsSubgroup'; assumption.
Defined.

Section SubgroupElements.
  Context {G : Group} (H : Subgroup G) (x y : G).
  Definition subgroup_in_unit : H mon_unit := issubgroup_in_unit.
  Definition subgroup_in_inv : H x -> H (- x) := issubgroup_in_inv x.
  Definition subgroup_in_inv' : H (- x) -> H x := issubgroup_in_inv' x.
  Definition subgroup_in_op : H x -> H y -> H (x * y) := issubgroup_in_op x y.
  Definition subgroup_in_op_inv : H x -> H y -> H (x * -y) := issubgroup_in_op_inv x y.
  Definition subgroup_in_inv_op : H x -> H y -> H (-x * y) := issubgroup_in_inv_op x y.
  Definition subgroup_in_op_l : H (x * y) -> H y -> H x := issubgroup_in_op_l x y.
  Definition subgroup_in_op_r : H (x * y) -> H x -> H y := issubgroup_in_op_r x y.
End SubgroupElements.

Global Instance isequiv_subgroup_in_inv `(H : Subgroup G) (x : G)
  : IsEquiv (subgroup_in_inv H x).
G: Group
H: Subgroup G
x: G
IsEquiv (subgroup_in_inv H x)
Proof.
G: Group
H: Subgroup G
x: G
IsEquiv (subgroup_in_inv H x)
  srapply isequiv_iff_hprop.
G: Group
H: Subgroup G
x: G
H (- x) -> H x
  apply subgroup_in_inv'.
Defined.

Definition equiv_subgroup_inverse {G : Group} (H : Subgroup G) (x : G)
  : H x <~> H (-x) := Build_Equiv _ _ (subgroup_in_inv H x) _.

(** The group given by a subgroup *)
Definition subgroup_group {G : Group} (H : Subgroup G) : Group.
G: Group
H: Subgroup G
Group
Proof.
G: Group
H: Subgroup G
Group
  apply (Build_Group
      (** The underlying type is the sigma type of the predicate. *)
      (sig H)
      (** The operation is the group operation on the first projection with the proof  of being in the subgroup given by the subgroup data. *)
      (fun '(x ; p) '(y ; q) => (x * y ; issubgroup_in_op x y p q))
      (** The unit *)
      (mon_unit ; issubgroup_in_unit)
      (** Inverse *)
      (fun '(x ; p) => (- x ; issubgroup_in_inv _ p))).
G: Group
H: Subgroup G
IsGroup {x : _ & H x}
  (** Finally we need to prove our group laws. *)
  repeat split.
G: Group
H: Subgroup G
IsHSet {x : _ & H x}
G: Group
H: Subgroup G
Associative sg_op
G: Group
H: Subgroup G
LeftIdentity sg_op mon_unit
G: Group
H: Subgroup G
RightIdentity sg_op mon_unit
G: Group
H: Subgroup G
LeftInverse sg_op negate mon_unit
G: Group
H: Subgroup G
RightInverse sg_op negate mon_unit
  1: exact _.
G: Group
H: Subgroup G
Associative sg_op
G: Group
H: Subgroup G
LeftIdentity sg_op mon_unit
G: Group
H: Subgroup G
RightIdentity sg_op mon_unit
G: Group
H: Subgroup G
LeftInverse sg_op negate mon_unit
G: Group
H: Subgroup G
RightInverse sg_op negate mon_unit
  all: grp_auto.
Defined.

Coercion subgroup_group : Subgroup >-> Group.

Definition subgroup_incl {G : Group} (H : Subgroup G)
  : subgroup_group H $-> G.
G: Group
H: Subgroup G
H $-> G
Proof.
G: Group
H: Subgroup G
H $-> G
  snrapply Build_GroupHomomorphism'.
G: Group
H: Subgroup G
H -> G
G: Group
H: Subgroup G
IsMonoidPreserving ?grp_homo_map
  1: exact pr1.
G: Group
H: Subgroup G
IsMonoidPreserving pr1
  repeat split.
Defined.

Global Instance isembedding_subgroup_incl {G : Group} (H : Subgroup G)
  : IsEmbedding (subgroup_incl H)
  := fun _ => istrunc_equiv_istrunc _ (hfiber_fibration _ _).

Definition issig_subgroup {G : Group} : _ <~> Subgroup G
  := ltac:(issig).

(** Trivial subgroup *)
Definition trivial_subgroup {G} : Subgroup G.
G: Group
Subgroup G
Proof.
G: Group
Subgroup G
  rapply (Build_Subgroup' (fun x => x = mon_unit)).
G: Group
mon_unit = mon_unit
G: Group
forall x y : G,
x = mon_unit -> y = mon_unit -> x * - y = mon_unit
  1: reflexivity.
G: Group
forall x y : G,
x = mon_unit -> y = mon_unit -> x * - y = mon_unit
  intros x y p q.
G: Group
x, y: G
p: x = mon_unit
q: y = mon_unit
x * - y = mon_unit
  rewrite p, q.
G: Group
x, y: G
p: x = mon_unit
q: y = mon_unit
mon_unit * - mon_unit = mon_unit
  rewrite left_identity.
G: Group
x, y: G
p: x = mon_unit
q: y = mon_unit
- mon_unit = mon_unit
  apply negate_mon_unit.
Defined.

(** Every group is a (maximal) subgroup of itself *)
Definition maximal_subgroup {G} : Subgroup G.
G: Group
Subgroup G
Proof.
G: Group
Subgroup G
  rapply (Build_Subgroup G (fun x => Unit)).
G: Group
IsSubgroup (fun _ : G => Unit)
  split; auto; exact _.
Defined.

(** Paths between subgroups correspond to homotopies between the underlying predicates. *) 
Proposition equiv_path_subgroup `{F : Funext} {G : Group} (H K : Subgroup G)
  : (H == K) <~> (H = K).
F: Funext
G: Group
H, K: Subgroup G
H == K <~> H = K
Proof.
F: Funext
G: Group
H, K: Subgroup G
H == K <~> H = K
  refine ((equiv_ap' issig_subgroup^-1%equiv _ _)^-1%equiv oE _); cbn.
F: Funext
G: Group
H, K: Subgroup G
H == K <~>
(H; subgroup_issubgroup G H) =
(K; subgroup_issubgroup G K)
  refine (equiv_path_sigma_hprop _ _ oE _); cbn.
F: Funext
G: Group
H, K: Subgroup G
H == K <~> H = K
  apply equiv_path_arrow.
Defined.

Proposition equiv_path_subgroup' `{U : Univalence} {G : Group} (H K : Subgroup G)
  : (forall g:G, H g <-> K g) <~> (H = K).
U: Univalence
G: Group
H, K: Subgroup G
(forall g : G, H g <-> K g) <~> H = K
Proof.
U: Univalence
G: Group
H, K: Subgroup G
(forall g : G, H g <-> K g) <~> H = K
  refine (equiv_path_subgroup _ _ oE _).
U: Univalence
G: Group
H, K: Subgroup G
(forall g : G, H g <-> K g) <~> H == K
  apply equiv_functor_forall_id; intro g.
U: Univalence
G: Group
H, K: Subgroup G
g: G
(H g <-> K g) <~> H g = K g
  exact equiv_path_iff_ishprop.
Defined.

Global Instance ishset_subgroup `{Univalence} {G : Group} : IsHSet (Subgroup G).
H: Univalence
G: Group
IsHSet (Subgroup G)
Proof.
H: Univalence
G: Group
IsHSet (Subgroup G)
  nrefine (istrunc_equiv_istrunc _ issig_subgroup).
H: Univalence
G: Group
IsHSet {H : G -> Type & IsSubgroup H}
  nrefine (istrunc_equiv_istrunc _ (equiv_functor_sigma_id _)).
H: Univalence
G: Group
forall a : G -> Type, ?Goal a <~> IsSubgroup a
H: Univalence
G: Group
IsHSet {x : _ & ?Goal x}
  -
H: Univalence
G: Group
forall a : G -> Type, ?Goal a <~> IsSubgroup a intro P; apply issig_issubgroup.
  -
H: Univalence
G: Group
IsHSet
  {P : G -> Type &
  {_ : forall x : G, IsHProp (P x) &
  {_ : P mon_unit &
  {_ : forall x y : G, P x -> P y -> P (x * y) &
  forall x : G, P x -> P (- x)}}}} nrefine (istrunc_equiv_istrunc _ (equiv_sigma_assoc' _ _)^-1%equiv).
H: Univalence
G: Group
IsHSet
  {ap : {a : G -> Type & forall x : G, IsHProp (a x)}
  &
  {_ : ap.1 mon_unit &
  {_
  : forall x y : G, ap.1 x -> ap.1 y -> ap.1 (x * y) &
  forall x : G, ap.1 x -> ap.1 (- x)}}}
    nrapply istrunc_sigma.
H: Univalence
G: Group
IsHSet {a : G -> Type & forall x : G, IsHProp (a x)}
H: Univalence
G: Group
forall
a : {a : G -> Type & forall x : G, IsHProp (a x)},
IsHSet
  {_ : a.1 mon_unit &
  {_ : forall x y : G, a.1 x -> a.1 y -> a.1 (x * y) &
  forall x : G, a.1 x -> a.1 (- x)}}
    2: intros []; apply istrunc_hprop.
H: Univalence
G: Group
IsHSet {a : G -> Type & forall x : G, IsHProp (a x)}
    nrefine (istrunc_equiv_istrunc
               _ (equiv_sig_coind (fun g:G => Type) (fun g x => IsHProp x))^-1%equiv).
H: Univalence
G: Group
IsHSet (G -> {x : Type & IsHProp x})
    apply istrunc_forall.
Defined.

Section Cosets.

  (** Left and right cosets give equivalence relations. *)

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

  (** The relation of being in a left coset represented by an element. *)
  Definition in_cosetL : Relation G := fun x y => H (-x * y).
  (** The relation of being in a right coset represented by an element. *)
  Definition in_cosetR : Relation G := fun x y => H (x * -y).

  Hint Extern 4 => progress unfold in_cosetL : typeclass_instances.
  Hint Extern 4 => progress unfold in_cosetR : typeclass_instances.

  Global Arguments in_cosetL /.
  Global Arguments in_cosetR /.

  (** These are props *)
  Global Instance ishprop_in_cosetL : is_mere_relation G in_cosetL := _.
  Global Instance ishprop_in_cosetR : is_mere_relation G in_cosetR := _.

  (** In fact, they are both equivalence relations. *)
  Global Instance reflexive_in_cosetL : Reflexive in_cosetL.
G: Group
H: Subgroup G
Reflexive in_cosetL
  Proof.
G: Group
H: Subgroup G
Reflexive in_cosetL
    intro x; hnf.
G: Group
H: Subgroup G
x: G
H (- x * x)
    rewrite left_inverse.
G: Group
H: Subgroup G
x: G
H mon_unit
    apply issubgroup_in_unit.
  Defined.

  Global Instance reflexive_in_cosetR : Reflexive in_cosetR.
G: Group
H: Subgroup G
Reflexive in_cosetR
  Proof.
G: Group
H: Subgroup G
Reflexive in_cosetR
    intro x; hnf.
G: Group
H: Subgroup G
x: G
H (x * - x)
    rewrite right_inverse.
G: Group
H: Subgroup G
x: G
H mon_unit
    apply issubgroup_in_unit.
  Defined.

  Global Instance symmetric_in_cosetL : Symmetric in_cosetL.
G: Group
H: Subgroup G
Symmetric in_cosetL
  Proof.
G: Group
H: Subgroup G
Symmetric in_cosetL
    intros x y h; cbn; cbn in h.
G: Group
H: Subgroup G
x, y: G
h: H (- x * y)
H (- y * x)
    rewrite <- (negate_involutive x).
G: Group
H: Subgroup G
x, y: G
h: H (- x * y)
H (- y * - - x)
    rewrite <- negate_sg_op.
G: Group
H: Subgroup G
x, y: G
h: H (- x * y)
H (- (- x * y))
    apply issubgroup_in_inv; assumption.
  Defined.

  Global Instance symmetric_in_cosetR : Symmetric in_cosetR.
G: Group
H: Subgroup G
Symmetric in_cosetR
  Proof.
G: Group
H: Subgroup G
Symmetric in_cosetR
    intros x y h; cbn; cbn in h.
G: Group
H: Subgroup G
x, y: G
h: H (x * - y)
H (y * - x)
    rewrite <- (negate_involutive y).
G: Group
H: Subgroup G
x, y: G
h: H (x * - y)
H (- - y * - x)
    rewrite <- negate_sg_op.
G: Group
H: Subgroup G
x, y: G
h: H (x * - y)
H (- (x * - y))
    apply issubgroup_in_inv; assumption.
  Defined.

  Global Instance transitive_in_cosetL : Transitive in_cosetL.
G: Group
H: Subgroup G
Transitive in_cosetL
  Proof.
G: Group
H: Subgroup G
Transitive in_cosetL
    intros x y z h k; cbn; cbn in h; cbn in k.
G: Group
H: Subgroup G
x, y, z: G
h: H (- x * y)
k: H (- y * z)
H (- x * z)
    rewrite <- (right_identity (-x)).
G: Group
H: Subgroup G
x, y, z: G
h: H (- x * y)
k: H (- y * z)
H (- x * mon_unit * z)
    rewrite <- (right_inverse y : y * -y = mon_unit).
G: Group
H: Subgroup G
x, y, z: G
h: H (- x * y)
k: H (- y * z)
H (- x * (y * - y) * z)
    rewrite (associativity (-x) _ _).
G: Group
H: Subgroup G
x, y, z: G
h: H (- x * y)
k: H (- y * z)
H (- x * y * - y * z)
    rewrite <- simple_associativity.
G: Group
H: Subgroup G
x, y, z: G
h: H (- x * y)
k: H (- y * z)
H (- x * y * (- y * z))
    apply issubgroup_in_op; assumption.
  Defined.

  Global Instance transitive_in_cosetR : Transitive in_cosetR.
G: Group
H: Subgroup G
Transitive in_cosetR
  Proof.
G: Group
H: Subgroup G
Transitive in_cosetR
    intros x y z h k; cbn; cbn in h; cbn in k.
G: Group
H: Subgroup G
x, y, z: G
h: H (x * - y)
k: H (y * - z)
H (x * - z)
    rewrite <- (right_identity x).
G: Group
H: Subgroup G
x, y, z: G
h: H (x * - y)
k: H (y * - z)
H (x * mon_unit * - z)
    rewrite <- (left_inverse y : -y * y = mon_unit).
G: Group
H: Subgroup G
x, y, z: G
h: H (x * - y)
k: H (y * - z)
H (x * (- y * y) * - z)
    rewrite (simple_associativity x).
G: Group
H: Subgroup G
x, y, z: G
h: H (x * - y)
k: H (y * - z)
H (x * - y * y * - z)
    rewrite <- (associativity _ _ (-z)).
G: Group
H: Subgroup G
x, y, z: G
h: H (x * - y)
k: H (y * - z)
H (x * - y * (y * - z))
    apply issubgroup_in_op; assumption.
  Defined.

End Cosets.

(** Identities related to the left and right cosets. *)

Definition in_cosetL_unit {G : Group} {N : Subgroup G}
  : forall x y, in_cosetL N (-x * y) mon_unit <~> in_cosetL N x y.
G: Group
N: Subgroup G
forall x y : G,
in_cosetL N (- x * y) mon_unit <~> in_cosetL N x y
Proof.
G: Group
N: Subgroup G
forall x y : G,
in_cosetL N (- x * y) mon_unit <~> in_cosetL N x y
  intros x y; cbn.
G: Group
N: Subgroup G
x, y: G
N (- (- x * y) * mon_unit) <~> N (- x * y)
  rewrite (right_identity (- _)).
G: Group
N: Subgroup G
x, y: G
N (- (- x * y)) <~> N (- x * y)
  rewrite (negate_sg_op _).
G: Group
N: Subgroup G
x, y: G
N (- y * - - x) <~> N (- x * y)
  rewrite (negate_involutive _).
G: Group
N: Subgroup G
x, y: G
N (- y * x) <~> N (- x * y)
  apply equiv_iff_hprop; apply symmetric_in_cosetL.
Defined.

Definition in_cosetR_unit {G : Group} {N : Subgroup G}
  : forall x y, in_cosetR N (x * -y) mon_unit <~> in_cosetR N x y.
G: Group
N: Subgroup G
forall x y : G,
in_cosetR N (x * - y) mon_unit <~> in_cosetR N x y
Proof.
G: Group
N: Subgroup G
forall x y : G,
in_cosetR N (x * - y) mon_unit <~> in_cosetR N x y
  intros x y; cbn.
G: Group
N: Subgroup G
x, y: G
N (x * - y * - mon_unit) <~> N (x * - y)
  rewrite negate_mon_unit.
G: Group
N: Subgroup G
x, y: G
N (x * - y * mon_unit) <~> N (x * - y)
  rewrite (right_identity (x * -y)).
G: Group
N: Subgroup G
x, y: G
N (x * - y) <~> N (x * - y)
  reflexivity.
Defined.

(** Symmetry is an equivalence. *)
Definition equiv_in_cosetL_symm {G : Group} {N : Subgroup G}
  : forall x y, in_cosetL N x y <~> in_cosetL N y x.
G: Group
N: Subgroup G
forall x y : G, in_cosetL N x y <~> in_cosetL N y x
Proof.
G: Group
N: Subgroup G
forall x y : G, in_cosetL N x y <~> in_cosetL N y x
  intros x y.
G: Group
N: Subgroup G
x, y: G
in_cosetL N x y <~> in_cosetL N y x
  srapply equiv_iff_hprop.
G: Group
N: Subgroup G
x, y: G
in_cosetL N x y -> in_cosetL N y x
G: Group
N: Subgroup G
x, y: G
in_cosetL N y x -> in_cosetL N x y
  all: by intro.
Defined.

Definition equiv_in_cosetR_symm {G : Group} {N : Subgroup G}
  : forall x y, in_cosetR N x y <~> in_cosetR N y x.
G: Group
N: Subgroup G
forall x y : G, in_cosetR N x y <~> in_cosetR N y x
Proof.
G: Group
N: Subgroup G
forall x y : G, in_cosetR N x y <~> in_cosetR N y x
  intros x y.
G: Group
N: Subgroup G
x, y: G
in_cosetR N x y <~> in_cosetR N y x
  srapply equiv_iff_hprop.
G: Group
N: Subgroup G
x, y: G
in_cosetR N x y -> in_cosetR N y x
G: Group
N: Subgroup G
x, y: G
in_cosetR N y x -> in_cosetR N x y
  all: by intro.
Defined.

(** A subgroup is normal if being in a left coset is equivalent to being in a right coset represented by the same element. *)
Class IsNormalSubgroup {G : Group} (N : Subgroup G)
  := isnormal : forall {x y}, in_cosetL N x y <~> in_cosetR N x y.

Record NormalSubgroup (G : Group) := {
  normalsubgroup_subgroup : Subgroup G ;
  normalsubgroup_isnormal : IsNormalSubgroup normalsubgroup_subgroup ;
}.

Coercion normalsubgroup_subgroup : NormalSubgroup >-> Subgroup.
Global Existing Instance normalsubgroup_isnormal.

(* Inverses are then respected *)
Definition in_cosetL_inverse {G : Group} {N : NormalSubgroup G}
  : forall x y : G, in_cosetL N (-x) (-y) <~> in_cosetL N x y.
G: Group
N: NormalSubgroup G
forall x y : G,
in_cosetL N (- x) (- y) <~> in_cosetL N x y
Proof.
G: Group
N: NormalSubgroup G
forall x y : G,
in_cosetL N (- x) (- y) <~> in_cosetL N x y
  intros x y.
G: Group
N: NormalSubgroup G
x, y: G
in_cosetL N (- x) (- y) <~> in_cosetL N x y
  unfold in_cosetL.
G: Group
N: NormalSubgroup G
x, y: G
N (- - x * - y) <~> N (- x * y)
  rewrite negate_involutive.
G: Group
N: NormalSubgroup G
x, y: G
N (x * - y) <~> N (- x * y)
  symmetry; apply isnormal.
Defined.

Definition in_cosetR_inverse {G : Group} {N : NormalSubgroup G}
  : forall x y : G, in_cosetR N (-x) (-y) <~> in_cosetR N x y.
G: Group
N: NormalSubgroup G
forall x y : G,
in_cosetR N (- x) (- y) <~> in_cosetR N x y
Proof.
G: Group
N: NormalSubgroup G
forall x y : G,
in_cosetR N (- x) (- y) <~> in_cosetR N x y
  intros x y.
G: Group
N: NormalSubgroup G
x, y: G
in_cosetR N (- x) (- y) <~> in_cosetR N x y
  refine (_ oE (in_cosetR_unit _ _)^-1).
G: Group
N: NormalSubgroup G
x, y: G
in_cosetR N (- x * - - y) mon_unit <~> in_cosetR N x y
  refine (_ oE isnormal^-1).
G: Group
N: NormalSubgroup G
x, y: G
in_cosetL N (- x * - - y) mon_unit <~> in_cosetR N x y
  refine (_ oE in_cosetL_unit _ _).
G: Group
N: NormalSubgroup G
x, y: G
in_cosetL N x (- - y) <~> in_cosetR N x y
  refine (_ oE isnormal).
G: Group
N: NormalSubgroup G
x, y: G
in_cosetR N x (- - y) <~> in_cosetR N x y
  by rewrite negate_involutive.
Defined.

(** This lets us prove that left and right coset relations are congruences. *)
Definition in_cosetL_cong {G : Group} {N : NormalSubgroup G}
  (x x' y y' : G)
  : in_cosetL N x y -> in_cosetL N x' y' -> in_cosetL N (x * x') (y * y').
G: Group
N: NormalSubgroup G
x, x', y, y': G
in_cosetL N x y ->
in_cosetL N x' y' -> in_cosetL N (x * x') (y * y')
Proof.
G: Group
N: NormalSubgroup G
x, x', y, y': G
in_cosetL N x y ->
in_cosetL N x' y' -> in_cosetL N (x * x') (y * y')
  cbn; intros p q.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (- x * y)
q: N (- x' * y')
N (- (x * x') * (y * y'))
  (** rewrite goal before applying subgroup_op *)
  rewrite negate_sg_op, <- simple_associativity.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (- x * y)
q: N (- x' * y')
N (- x' * (- x * (y * y')))
  apply symmetric_in_cosetL; cbn.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (- x * y)
q: N (- x' * y')
N (- (- x * (y * y')) * x')
  rewrite simple_associativity.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (- x * y)
q: N (- x' * y')
N (- (- x * y * y') * x')
  apply isnormal; cbn.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (- x * y)
q: N (- x' * y')
N (- x * y * y' * - x')
  rewrite <- simple_associativity.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (- x * y)
q: N (- x' * y')
N (- x * y * (y' * - x'))
  apply subgroup_in_op.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (- x * y)
q: N (- x' * y')
N (- x * y)
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (- x * y)
q: N (- x' * y')
N (y' * - x')
  1: assumption.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (- x * y)
q: N (- x' * y')
N (y' * - x')
  by apply isnormal, symmetric_in_cosetL.
Defined.

Definition in_cosetR_cong  {G : Group} {N : NormalSubgroup G}
  (x x' y y' : G)
  : in_cosetR N x y -> in_cosetR N x' y' -> in_cosetR N (x * x') (y * y').
G: Group
N: NormalSubgroup G
x, x', y, y': G
in_cosetR N x y ->
in_cosetR N x' y' -> in_cosetR N (x * x') (y * y')
Proof.
G: Group
N: NormalSubgroup G
x, x', y, y': G
in_cosetR N x y ->
in_cosetR N x' y' -> in_cosetR N (x * x') (y * y')
  cbn; intros p q.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * - y)
q: N (x' * - y')
N (x * x' * - (y * y'))
  (** rewrite goal before applying subgroup_op *)
  rewrite negate_sg_op, simple_associativity.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * - y)
q: N (x' * - y')
N (x * x' * - y' * - y)
  apply symmetric_in_cosetR; cbn.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * - y)
q: N (x' * - y')
N (y * - (x * x' * - y'))
  rewrite <- simple_associativity.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * - y)
q: N (x' * - y')
N (y * - (x * (x' * - y')))
  apply isnormal; cbn.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * - y)
q: N (x' * - y')
N (- y * (x * (x' * - y')))
  rewrite simple_associativity.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * - y)
q: N (x' * - y')
N (- y * x * (x' * - y'))
  apply subgroup_in_op.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * - y)
q: N (x' * - y')
N (- y * x)
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * - y)
q: N (x' * - y')
N (x' * - y')
  2: assumption.
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * - y)
q: N (x' * - y')
N (- y * x)
  by apply isnormal, symmetric_in_cosetR.
Defined.

(** The property of being the trivial subgroup is useful. *)
Definition IsTrivialSubgroup {G : Group} (H : Subgroup G) : Type :=
  forall x, H x <-> trivial_subgroup x.
Existing Class IsTrivialSubgroup.

Global Instance istrivialsubgroup_trivial_subgroup {G : Group}
  : IsTrivialSubgroup (@trivial_subgroup G)
  := ltac:(hnf; reflexivity).

(** Intersection of two subgroups *)
Definition subgroup_intersection {G : Group} (H K : Subgroup G) : Subgroup G.
G: Group
H, K: Subgroup G
Subgroup G
Proof.
G: Group
H, K: Subgroup G
Subgroup G
  snrapply Build_Subgroup'.
G: Group
H, K: Subgroup G
G -> Type
G: Group
H, K: Subgroup G
forall x : G, IsHProp (?H x)
G: Group
H, K: Subgroup G
?H mon_unit
G: Group
H, K: Subgroup G
forall x y : G, ?H x -> ?H y -> ?H (x * - y)
  1: exact (fun g => H g /\ K g).
G: Group
H, K: Subgroup G
forall x : G,
IsHProp ((fun g : G => (H g * K g)%type) x)
G: Group
H, K: Subgroup G
(fun g : G => (H g * K g)%type) mon_unit
G: Group
H, K: Subgroup G
forall x y : G,
(fun g : G => (H g * K g)%type) x ->
(fun g : G => (H g * K g)%type) y ->
(fun g : G => (H g * K g)%type) (x * - y)
  1: exact _.
G: Group
H, K: Subgroup G
(fun g : G => (H g * K g)%type) mon_unit
G: Group
H, K: Subgroup G
forall x y : G,
(fun g : G => (H g * K g)%type) x ->
(fun g : G => (H g * K g)%type) y ->
(fun g : G => (H g * K g)%type) (x * - y)
  1: split; apply subgroup_in_unit.
G: Group
H, K: Subgroup G
forall x y : G,
(fun g : G => (H g * K g)%type) x ->
(fun g : G => (H g * K g)%type) y ->
(fun g : G => (H g * K g)%type) (x * - y)
  intros x y [] [].
G: Group
H, K: Subgroup G
x, y: G
fst: H x
snd: K x
fst0: H y
snd0: K y
(H (sg_op x (- y)) * K (sg_op x (- y)))%type
  split; by apply subgroup_in_op_inv.
Defined.

(** *** The subgroup generated by a subset *)

(** Underlying type family of a subgroup generated by subset *)
Inductive subgroup_generated_type {G : Group} (X : G -> Type) : G -> Type :=
(** The subgroup should contain all elements of the original family. *)
| sgt_in (g : G) : X g -> subgroup_generated_type X g
(** It should contain the unit. *)
| sgt_unit : subgroup_generated_type X mon_unit
(** Finally, it should be closed under inverses and operation. *)
| sgt_op (g h : G)
  : subgroup_generated_type X g
  -> subgroup_generated_type X h
  -> subgroup_generated_type X (g * - h)
.

Arguments sgt_in {G X g}.
Arguments sgt_unit {G X}.
Arguments sgt_op {G X g h}.

(** Note that [subgroup_generated_type] will not automatically land in [HProp]. For example, if [X] already "contains" the unit of the group, then there are at least two different inhabitants of this family at the unit (given by [sgt_unit] and [sgt_in group_unit _]). Therefore, we propositionally truncate in [subgroup_generated] below. *)

(** Subgroups are closed under inverses. *)
Definition sgt_inv {G : Group} {X} {g : G}
  : subgroup_generated_type X g -> subgroup_generated_type X (- g).
G: Group
X: G -> Type
g: G
subgroup_generated_type X g ->
subgroup_generated_type X (- g)
Proof.
G: Group
X: G -> Type
g: G
subgroup_generated_type X g ->
subgroup_generated_type X (- g)
  intros p.
G: Group
X: G -> Type
g: G
p: subgroup_generated_type X g
subgroup_generated_type X (- g)
  rewrite <- left_identity.
G: Group
X: G -> Type
g: G
p: subgroup_generated_type X g
subgroup_generated_type X (mon_unit * - g)
  exact (sgt_op sgt_unit p).
Defined.

Definition sgt_op' {G : Group} {X} {g h : G}
  : subgroup_generated_type X g
    -> subgroup_generated_type X h
    -> subgroup_generated_type X (g * h).
G: Group
X: G -> Type
g, h: G
subgroup_generated_type X g ->
subgroup_generated_type X h ->
subgroup_generated_type X (g * h)
Proof.
G: Group
X: G -> Type
g, h: G
subgroup_generated_type X g ->
subgroup_generated_type X h ->
subgroup_generated_type X (g * h)
  intros p q.
G: Group
X: G -> Type
g, h: G
p: subgroup_generated_type X g
q: subgroup_generated_type X h
subgroup_generated_type X (g * h)
  rewrite <- (negate_involutive h).
G: Group
X: G -> Type
g, h: G
p: subgroup_generated_type X g
q: subgroup_generated_type X h
subgroup_generated_type X (g * - - h)
  exact (sgt_op p (sgt_inv q)).
Defined.

(** The subgroup generated by a subset *)
Definition subgroup_generated {G : Group} (X : G -> Type) : Subgroup G.
G: Group
X: G -> Type
Subgroup G
Proof.
G: Group
X: G -> Type
Subgroup G
  refine (Build_Subgroup' (merely o subgroup_generated_type X)
            (tr sgt_unit) _).
G: Group
X: G -> Type
forall x y : G,
merely (subgroup_generated_type X x) ->
merely (subgroup_generated_type X y) ->
merely (subgroup_generated_type X (x * - y))
  intros x y p q; strip_truncations.
G: Group
X: G -> Type
x, y: G
q: subgroup_generated_type X y
p: subgroup_generated_type X x
merely (subgroup_generated_type X (x * - y))
  exact (tr (sgt_op p q)).
Defined.

(** The inclusion of generators into the generated subgroup. *)
Definition subgroup_generated_gen_incl {G : Group} {X : G -> Type} (g : G) (H : X g)
  : subgroup_generated X
  := (g; tr (sgt_in H)).

(** If [f : G $-> H] is a group homomorphism and [X] and [Y] are subsets of [G] and [H] such that [f] maps [X] into [Y], then [f] sends the subgroup generated by [X] into the subgroup generated by [Y]. *)
Definition functor_subgroup_generated {G H : Group} (X : G -> Type) (Y : H -> Type)
  (f : G $-> H) (preserves : forall g, X g -> Y (f g))
  : forall g, subgroup_generated X g -> subgroup_generated Y (f g).
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
forall g : G,
subgroup_generated X g -> subgroup_generated Y (f g)
Proof.
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
forall g : G,
subgroup_generated X g -> subgroup_generated Y (f g)
  intro g.
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
g: G
subgroup_generated X g -> subgroup_generated Y (f g)
  apply Trunc_functor.
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
g: G
subgroup_generated_type X g ->
subgroup_generated_type Y (f g)
  intro p.
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
g: G
p: subgroup_generated_type X g
subgroup_generated_type Y (f g)
  induction p as [g i | | g h p1 IHp1 p2 IHp2].
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
g: G
i: X g
subgroup_generated_type Y (f g)
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
subgroup_generated_type Y (f mon_unit)
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
g, h: G
p1: subgroup_generated_type X g
p2: subgroup_generated_type X h
IHp1: subgroup_generated_type Y (f g)
IHp2: subgroup_generated_type Y (f h)
subgroup_generated_type Y (f (g * - h))
  -
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
g: G
i: X g
subgroup_generated_type Y (f g) apply sgt_in, preserves, i.
  -
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
subgroup_generated_type Y (f mon_unit) rewrite grp_homo_unit.
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
subgroup_generated_type Y mon_unit
    apply sgt_unit.
  -
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
g, h: G
p1: subgroup_generated_type X g
p2: subgroup_generated_type X h
IHp1: subgroup_generated_type Y (f g)
IHp2: subgroup_generated_type Y (f h)
subgroup_generated_type Y (f (g * - h)) rewrite grp_homo_op, grp_homo_inv.
G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
g, h: G
p1: subgroup_generated_type X g
p2: subgroup_generated_type X h
IHp1: subgroup_generated_type Y (f g)
IHp2: subgroup_generated_type Y (f h)
subgroup_generated_type Y (f g * - f h)
    by apply sgt_op.
Defined.

(** The product of two subgroups. *)
Definition subgroup_product {G : Group} (H K : Subgroup G) : Subgroup G
  := subgroup_generated (fun x => ((H x) + (K x))%type).

(** The induction principle for the product. *)
Definition subgroup_product_ind {G : Group} (H K : Subgroup G)
  (P : forall x, subgroup_product H K x -> Type)
  (P_H_in : forall x y, P x (tr (sgt_in (inl y))))
  (P_K_in : forall x y, P x (tr (sgt_in (inr y))))
  (P_unit : P mon_unit (tr sgt_unit))
  (P_op : forall x y h k, P x (tr h) -> P y (tr k) -> P (x * - y) (tr (sgt_op h k)))
  `{forall x y, IsHProp (P x y)}
  : forall x (p : subgroup_product H K x), P x p.
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
forall (x : G) (p : subgroup_product H K x), P x p
Proof.
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
forall (x : G) (p : subgroup_product H K x), P x p
  intros x p.
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
p: subgroup_product H K x
P x p
  strip_truncations.
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
p: subgroup_generated_type
  (fun x : G => (H x + K x)%type) x
P x (tr p)
  induction p as [x s | | x y h IHh k IHk].
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
s: (H x + K x)%type
P x (tr (sgt_in s))
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
P mon_unit (tr sgt_unit)
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x, y: G
h: subgroup_generated_type
  (fun x : G => (H x + K x)%type) x
k: subgroup_generated_type
  (fun x : G => (H x + K x)%type) y
IHh: P x (tr h)
IHk: P y (tr k)
P (x * - y) (tr (sgt_op h k))
  +
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
s: (H x + K x)%type
P x (tr (sgt_in s)) destruct s.
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
s: H x
P x (tr (sgt_in (inl s)))
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
s: K x
P x (tr (sgt_in (inr s)))
    -
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
s: H x
P x (tr (sgt_in (inl s))) apply P_H_in.
    -
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
s: K x
P x (tr (sgt_in (inr s))) apply P_K_in.
  +
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
P mon_unit (tr sgt_unit) exact P_unit.
  +
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P mon_unit (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x, y: G
h: subgroup_generated_type
  (fun x : G => (H x + K x)%type) x
k: subgroup_generated_type
  (fun x : G => (H x + K x)%type) y
IHh: P x (tr h)
IHk: P y (tr k)
P (x * - y) (tr (sgt_op h k)) by apply P_op.
Defined.

(* **** Paths between generated subgroups *)

(* This gets used twice in [path_subgroup_generated], so we factor it out here. *)
Local Lemma path_subgroup_generated_helper {G : Group}
  (X Y : G -> Type) (K : forall g, merely (X g) -> merely (Y g))
  : forall g, Trunc (-1) (subgroup_generated_type X g)
         -> Trunc (-1) (subgroup_generated_type Y g).
G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
forall g : G,
Trunc (-1) (subgroup_generated_type X g) ->
Trunc (-1) (subgroup_generated_type Y g)
Proof.
G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
forall g : G,
Trunc (-1) (subgroup_generated_type X g) ->
Trunc (-1) (subgroup_generated_type Y g)
  intro g; apply Trunc_rec; intro ing.
G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
g: G
ing: subgroup_generated_type X g
Trunc (-1) (subgroup_generated_type Y g)
  induction ing as [g x| |g h Xg IHYg Xh IHYh].
G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
g: G
x: X g
Trunc (-1) (subgroup_generated_type Y g)
G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
Trunc (-1) (subgroup_generated_type Y mon_unit)
G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
g, h: G
Xg: subgroup_generated_type X g
Xh: subgroup_generated_type X h
IHYg: Trunc (-1) (subgroup_generated_type Y g)
IHYh: Trunc (-1) (subgroup_generated_type Y h)
Trunc (-1) (subgroup_generated_type Y (g * - h))
  -
G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
g: G
x: X g
Trunc (-1) (subgroup_generated_type Y g) exact (Trunc_functor (-1) sgt_in (K g (tr x))).
  -
G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
Trunc (-1) (subgroup_generated_type Y mon_unit) exact (tr sgt_unit).
  -
G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
g, h: G
Xg: subgroup_generated_type X g
Xh: subgroup_generated_type X h
IHYg: Trunc (-1) (subgroup_generated_type Y g)
IHYh: Trunc (-1) (subgroup_generated_type Y h)
Trunc (-1) (subgroup_generated_type Y (g * - h)) strip_truncations.
G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
g, h: G
Xg: subgroup_generated_type X g
Xh: subgroup_generated_type X h
IHYh: subgroup_generated_type Y h
IHYg: subgroup_generated_type Y g
Trunc (-1) (subgroup_generated_type Y (g * - h))
    by apply tr, sgt_op.
Defined.

(* If the predicates selecting the generators are merely equivalent, then the generated subgroups are equal. (One could probably prove that the generated subgroup are isomorphic without using univalence.) *)
Definition path_subgroup_generated `{Univalence} {G : Group}
  (X Y : G -> Type) (K : forall g, Trunc (-1) (X g) <-> Trunc (-1) (Y g))
  : subgroup_generated X = subgroup_generated Y.
H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
subgroup_generated X = subgroup_generated Y
Proof.
H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
subgroup_generated X = subgroup_generated Y
  rapply equiv_path_subgroup'. (* Uses Univalence. *)
H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
forall g : G,
subgroup_generated X g <-> subgroup_generated Y g
  intro g; split.
H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
g: G
subgroup_generated X g -> subgroup_generated Y g
H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
g: G
subgroup_generated Y g -> subgroup_generated X g
  -
H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
g: G
subgroup_generated X g -> subgroup_generated Y g apply path_subgroup_generated_helper, (fun x => fst (K x)).
  -
H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
g: G
subgroup_generated Y g -> subgroup_generated X g apply path_subgroup_generated_helper, (fun x => snd (K x)).
Defined.

(* Equal subgroups have isomorphic underlying groups. *)
Definition equiv_subgroup_group {G : Group} (H1 H2 : Subgroup G)
  : H1 = H2 -> GroupIsomorphism H1 H2
  := ltac:(intros []; exact grp_iso_id).