Group.v

Require Import Basics Types HProp HFiber HSet.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Homotopy.IdentitySystems.
Require Import (notations) Classes.interfaces.canonical_names.
Require Export (hints) Classes.interfaces.abstract_algebra.
Require Export (hints) Classes.interfaces.canonical_names.
(** We only export the parts of these that will be most useful to users of this file. *)
Require Export Classes.interfaces.canonical_names (SgOp, sg_op, MonUnit, mon_unit,
    LeftIdentity, left_identity, RightIdentity, right_identity,
    Inverse, inv, Associative, simple_associativity, associativity, associative_flip,
    LeftInverse, left_inverse, RightInverse, right_inverse, Commutative, commutativity).
Export canonical_names.BinOpNotations.
Require Export Classes.interfaces.abstract_algebra (IsGroup(..), group_monoid, inverse_l, inverse_r,
    IsSemiGroup(..), sg_set, sg_ass,
    IsMonoid(..), monoid_left_id, monoid_right_id, monoid_semigroup,
    IsMonoidPreserving(..), monmor_unitmor, monmor_sgmor,
    IsSemiGroupPreserving, preserves_sg_op, IsUnitPreserving, preserves_mon_unit).
Require Export Classes.theory.groups.
Require Import Pointed.Core.
Require Import WildCat.
Require Import Spaces.Nat.Core Spaces.Int.
Require Import Truncations.Core.

Local Set Polymorphic Inductive Cumulativity.

Generalizable Variables G H A B C f g.

Declare Scope group_scope.

(** * Groups *)

(** A group is an abstraction of several common situations in mathematics. For example, consider the symmetries of an object.  Two symmetries can be combined; there is a symmetry that does nothing; and any symmetry can be reversed. Such situations arise in geometry, algebra and, importantly for us, homotopy theory. *)

Local Open Scope pointed_scope.
Local Open Scope mc_mult_scope.
Local Open Scope wc_iso_scope.

(** ** Definition of a Group *)

(** A group consists of a type, an operation on that type, a unit and an inverse that satisfy the group axioms in [IsGroup]. *)
Record Group := Build_Group_internal {
  group_type :> Type;
  group_sgop :: SgOp group_type;
  group_unit :: MonUnit group_type;
  group_inverse :: Inverse group_type;
  group_isgroup :: IsGroup group_type;
  (** This axiom is redundant, but will allow the "opposite" group to be definitionally involutive. *)
  group_assoc_opp : Associative (flip group_sgop);
}.

Arguments group_sgop {_}.
Arguments group_unit {_}.
Arguments group_inverse {_}.
Arguments group_isgroup {_}.
Arguments group_assoc_opp {_}.
(** We should never need to unfold the proof that something is a group. *)
Global Opaque group_isgroup.

Definition issig_group : _ <~> Group
  := ltac:(issig).

(** This is the main constructor that is used to build groups.

It differs from [Build_Group_internal] by removing the redundant second proof of associativity. There is a technical reason for keeping the second axiom around, see the definition of [grp_op].

Note that we could have given the fields of [IsGroup] in a completely unbundled manner, but this has a negative impact on performance since every time a [Group] term is unfolded, the axioms appear in the arguments.

It is therefore advised to use this constructor in combination with a tactic like [repeat split] when building groups. *)
Definition Build_Group (G : Type)
  `(op : SgOp G, unit : MonUnit G, inv : Inverse G, grp : !IsGroup G)
  : Group.G: Type
op: SgOp G
unit: MonUnit G
inv: Inverse G
grp: IsGroup G
Group
Proof.G: Type
op: SgOp G
unit: MonUnit G
inv: Inverse G
grp: IsGroup G
Group
  napply (Build_Group_internal G op unit inv grp).G: Type
op: SgOp G
unit: MonUnit G
inv: Inverse G
grp: IsGroup G
Associative (flip op)
  rapply associative_flip.
Defined.

(** ** Proof automation *)
(** Many times in group theoretic proofs we want some form of automation for obvious identities. Here we implement such a behavior. *)

(** We create a database of hints for the group theory library *)
Create HintDb group_db.

(** Our group laws can be proven easily with tactics such as [rapply associativity]. However this requires a typeclass search on more general algebraic structures. Therefore we explicitly list many groups laws here so that Coq can use them. We also create hints for each law in our groups database. *)
Section GroupLaws.
  Context {G : Group} (x y z : G).

  Definition grp_assoc := associativity x y z.
  Definition grp_unit_l := left_identity x.
  Definition grp_unit_r := right_identity x.
  Definition grp_inv_l := left_inverse x.
  Definition grp_inv_r := right_inverse x.

End GroupLaws.

#[export] Hint Immediate grp_assoc  : group_db.
#[export] Hint Immediate grp_unit_l : group_db.
#[export] Hint Immediate grp_unit_r : group_db.
#[export] Hint Immediate grp_inv_l  : group_db.
#[export] Hint Immediate grp_inv_r  : group_db.

(** Given path types in a product we may want to decompose. *)
#[export] Hint Extern 5 (@paths (_ * _) _ _) => (apply path_prod) : group_db.
(** Given path types in a sigma type of a hprop family (i.e. a subset) we may want to decompose. *)
#[export] Hint Extern 6 (@paths (sig _) _ _) => (rapply path_sigma_hprop) : group_db.

(** We also declare a tactic (notation) for automatically solving group laws *)
(** TODO: improve this tactic so that it also rewrites and is able to solve basic group lemmas. *)
Tactic Notation "grp_auto" := hnf; intros; eauto with group_db.

(** ** Some basic properties of groups *)

(** Groups are pointed sets with point the identity. *)
Instance ispointed_group (G : Group)
  : IsPointed G := @mon_unit G _.

Definition ptype_group : Group -> pType
  := fun G => [G, _].

Coercion ptype_group : Group >-> pType.
(** An element acting like the identity is unique. *)
Definition identity_unique {A : Type} {Aop : SgOp A}
  (x y : A) {p : LeftIdentity Aop x} {q : RightIdentity Aop y}
  : x = y := (q x)^ @ p y.

Definition identity_unique' {A : Type} {Aop : SgOp A}
  (x y : A) {p : LeftIdentity Aop x} {q : RightIdentity Aop y}
  : y = x := (identity_unique x y)^.

(** An element acting like an inverse is unique. *)
Definition inverse_unique `{IsMonoid A}
  (a x y : A) {p : x * a = mon_unit} {q : a * y = mon_unit}
  : x = y.A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
a, x, y: A
p: x * a = 1
q: a * y = 1
x = y
Proof.A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
a, x, y: A
p: x * a = 1
q: a * y = 1
x = y
  refine ((right_identity x)^ @ ap _ q^ @ _).A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
a, x, y: A
p: x * a = 1
q: a * y = 1
x * (a * y) = y
  refine (associativity _ _ _ @ _).A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
a, x, y: A
p: x * a = 1
q: a * y = 1
x * a * y = y
  refine (ap (fun x => x * y) p @ _).A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
a, x, y: A
p: x * a = 1
q: a * y = 1
1 * y = y
  apply left_identity.
Defined.

(** With other assumptions, the right inverse law follows from the left inverse law. *)
Definition right_inverse_left_inverse (G : Type) `{IsHSet G}
  `(SgOp G, MonUnit G, Inverse G, !Associative (.*.),
    !LeftIdentity (.*.) mon_unit,
    !LeftInverse (.*.) (^) mon_unit)
  : RightInverse (.*.) (^) mon_unit.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
RightInverse sg_op inv 1
Proof.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
RightInverse sg_op inv 1
  intros x.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
x * x^ = 1
  lhs_V rapply left_identity.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
1 * (x * x^) = 1
  apply (transport (fun x => x * _ = x) (left_inverse x^)).G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
(x^)^ * x^ * (x * x^) = (x^)^ * x^
  lhs_V rapply simple_associativity.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
(x^)^ * (x^ * (x * x^)) = (x^)^ * x^
  napply ap.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
x^ * (x * x^) = x^
  lhs rapply simple_associativity.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
x^ * x * x^ = x^
  lhs napply (ap (.* x^)).G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
x^ * x = ?Goal
G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
?Goal * x^ = x^
  1: apply left_inverse.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
1 * x^ = x^
  apply left_identity.
Defined.
Global Opaque right_inverse_left_inverse.

(** With other assumptions, the right identity law follows from the left identity law. *)
Definition right_identity_left_identity (G : Type) `{IsHSet G}
  `(SgOp G, MonUnit G, Inverse G, !Associative (.*.),
    !LeftIdentity (.*.) mon_unit,
    !LeftInverse (.*.) (^) mon_unit)
  : RightIdentity (.*.) mon_unit.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
RightIdentity sg_op 1
Proof.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
RightIdentity sg_op 1
  intros x.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
x * 1 = x
  lhs_V rapply left_identity.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
1 * (x * 1) = x
  rhs_V rapply left_identity.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
1 * (x * 1) = 1 * x
  apply (transport (fun x => x * _ = x * _) (left_inverse x^)).G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
(x^)^ * x^ * (x * 1) = (x^)^ * x^ * x
  lhs_V rapply simple_associativity.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
(x^)^ * (x^ * (x * 1)) = (x^)^ * x^ * x
  rhs_V rapply simple_associativity.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
(x^)^ * (x^ * (x * 1)) = (x^)^ * (x^ * x)
  napply ap.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
x^ * (x * 1) = x^ * x
  lhs rapply simple_associativity.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
x^ * x * 1 = x^ * x
  lhs exact (ap (.* mon_unit) (left_inverse x)).G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
1 * 1 = x^ * x
  lhs apply left_identity.G: Type
IsHSet0: IsHSet G
H: SgOp G
H0: MonUnit G
H1: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op inv 1
x: G
1 = x^ * x
  symmetry; apply left_inverse.
Defined.
Global Opaque right_identity_left_identity.

(** When building a group we can choose to omit the right inverse law and right identity law, since they follow from the left ones. Note that as before with [Build_Group], the extra associativity axiom is omitted. *)
Definition Build_Group' (G : Type) `{IsHSet G}
  `(op : SgOp G, unit : MonUnit G, inv : Inverse G, !Associative (.*.),
    !LeftIdentity (.*.) mon_unit, !LeftInverse (.*.) (^) mon_unit)
  : Group.G: Type
IsHSet0: IsHSet G
op: SgOp G
unit: MonUnit G
inv: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op canonical_names.inv 1
Group
Proof.G: Type
IsHSet0: IsHSet G
op: SgOp G
unit: MonUnit G
inv: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op canonical_names.inv 1
Group
  snapply (Build_Group G op unit inv); repeat split.G: Type
IsHSet0: IsHSet G
op: SgOp G
unit: MonUnit G
inv: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op canonical_names.inv 1
IsHSet G
G: Type
IsHSet0: IsHSet G
op: SgOp G
unit: MonUnit G
inv: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op canonical_names.inv 1
Associative sg_op
G: Type
IsHSet0: IsHSet G
op: SgOp G
unit: MonUnit G
inv: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op canonical_names.inv 1
LeftIdentity sg_op 1
G: Type
IsHSet0: IsHSet G
op: SgOp G
unit: MonUnit G
inv: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op canonical_names.inv 1
RightIdentity sg_op 1
G: Type
IsHSet0: IsHSet G
op: SgOp G
unit: MonUnit G
inv: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op canonical_names.inv 1
LeftInverse sg_op canonical_names.inv 1
G: Type
IsHSet0: IsHSet G
op: SgOp G
unit: MonUnit G
inv: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op canonical_names.inv 1
RightInverse sg_op canonical_names.inv 1
  1-3, 5: exact _.G: Type
IsHSet0: IsHSet G
op: SgOp G
unit: MonUnit G
inv: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op canonical_names.inv 1
RightIdentity sg_op 1
G: Type
IsHSet0: IsHSet G
op: SgOp G
unit: MonUnit G
inv: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op canonical_names.inv 1
RightInverse sg_op canonical_names.inv 1
  -G: Type
IsHSet0: IsHSet G
op: SgOp G
unit: MonUnit G
inv: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op canonical_names.inv 1
RightIdentity sg_op 1 napply right_identity_left_identity; exact _.
  -G: Type
IsHSet0: IsHSet G
op: SgOp G
unit: MonUnit G
inv: Inverse G
Associative0: Associative sg_op
LeftIdentity0: LeftIdentity sg_op 1
LeftInverse0: LeftInverse sg_op canonical_names.inv 1
RightInverse sg_op canonical_names.inv 1 napply right_inverse_left_inverse; exact _.
Defined.

(** This is a variant of [issig_group] that drops the opposite axiom. *)
Definition issig_group' `{Funext}
  : {G : Type & {op : SgOp G & {unit : MonUnit G & {inv : Inverse G
    & @IsGroup G op unit inv}}}}
   <~> Group.H: Funext
{G : Type &
{op : SgOp G &
{unit : MonUnit G & {inv : Inverse G & IsGroup G}}}} <~>
Group
Proof.H: Funext
{G : Type &
{op : SgOp G &
{unit : MonUnit G & {inv : Inverse G & IsGroup G}}}} <~>
Group
  nrefine (issig_group oE _^-1).H: Funext
{H : Type &
{H0 : SgOp H &
{H1 : MonUnit H &
{H2 : Inverse H &
{_ : IsGroup H & Associative (flip H0)}}}}} <~>
{G : Type &
{op : SgOp G &
{unit : MonUnit G & {inv : Inverse G & IsGroup G}}}}
  napply equiv_functor_sigma_id; intros G.H: Funext
G: Type
{H0 : SgOp G &
{H1 : MonUnit G &
{H2 : Inverse G &
{_ : IsGroup G & Associative (flip H0)}}}} <~>
{op : SgOp G &
{unit : MonUnit G & {inv : Inverse G & IsGroup G}}}
  napply equiv_functor_sigma_id; intros op.H: Funext
G: Type
op: SgOp G
{H1 : MonUnit G &
{H2 : Inverse G &
{_ : IsGroup G & Associative (flip op)}}} <~>
{unit : MonUnit G & {inv : Inverse G & IsGroup G}}
  napply equiv_functor_sigma_id; intros unit.H: Funext
G: Type
op: SgOp G
unit: MonUnit G
{H2 : Inverse G &
{_ : IsGroup G & Associative (flip op)}} <~>
{inv : Inverse G & IsGroup G}
  napply equiv_functor_sigma_id; intros inv; simpl.H: Funext
G: Type
op: SgOp G
unit: MonUnit G
inv: Inverse G
{_ : IsGroup G & Associative (flip op)} <~> IsGroup G
  rapply (equiv_iff_hprop pr1 (fun g => (g; _))).H: Funext
G: Type
op: SgOp G
unit: MonUnit G
inv: Inverse G
g: IsGroup G
Associative (flip op)
  intros z y x; symmetry; rapply simple_associativity.
Defined.

(** ** Group homomorphisms *)

(** Group homomorphisms are maps between groups that preserve the group operation. They allow us to compare groups and map their structure to one another. This is useful for determining if two groups are really the same, in which case we say they are "isomorphic". *)

(** A group homomorphism consists of a map between groups and a proof that the map preserves the group operation. *)
Record GroupHomomorphism (G H : Group) := Build_GroupHomomorphism {
  grp_homo_map :> group_type G -> group_type H;
  issemigrouppreserving_grp_homo :: IsSemiGroupPreserving grp_homo_map;
}.

Arguments grp_homo_map {G H}.
Arguments Build_GroupHomomorphism {G H} _ _.
Arguments issemigrouppreserving_grp_homo {G H} f _ : rename.

(** ** Basic properties of group homomorphisms *)

(** Group homomorphisms preserve group operations. This is an alias for [issemigrouppreserving_grp_homo] with the identity written explicitly. *)
Definition grp_homo_op
  : forall {G H : Group} (f : GroupHomomorphism G H) (x y : G), f (x * y) = f x * f y
  := @issemigrouppreserving_grp_homo.
#[export] Hint Immediate grp_homo_op : group_db.

(** Group homomorphisms are unit preserving. *)
Instance isunitpreserving_grp_homo {G H : Group}
  (f : GroupHomomorphism G H)
  : IsUnitPreserving f.G, H: Group
f: GroupHomomorphism G H
IsUnitPreserving f
Proof.G, H: Group
f: GroupHomomorphism G H
IsUnitPreserving f
  unfold IsUnitPreserving.G, H: Group
f: GroupHomomorphism G H
f 1 = 1
  apply (group_cancelL (f mon_unit)).G, H: Group
f: GroupHomomorphism G H
f 1 * f 1 = f 1 * 1
  rhs napply grp_unit_r.G, H: Group
f: GroupHomomorphism G H
f 1 * f 1 = f 1
  rhs_V rapply (ap  _ (monoid_left_id _ mon_unit)).G, H: Group
f: GroupHomomorphism G H
f 1 * f 1 = f (1 * 1)
  symmetry.G, H: Group
f: GroupHomomorphism G H
f (1 * 1) = f 1 * f 1
  napply issemigrouppreserving_grp_homo.
Defined.
(** We usually don't need access to the proof, so we mark this as opaque for a very slight speedup. *)
Opaque isunitpreserving_grp_homo.

(** Group homomorphisms preserve identities. This is an alias for the previous statement. *)
Definition grp_homo_unit
  : forall {G H : Group} (f : GroupHomomorphism G H), f mon_unit = mon_unit
  := @isunitpreserving_grp_homo.
#[export] Hint Immediate grp_homo_unit : group_db.

(** Therefore, group homomorphisms are monoid homomorphisms. *)
Instance ismonoidpreserving_grp_homo {G H : Group}
  (f : GroupHomomorphism G H)
  : IsMonoidPreserving f
  := {}.

(** Group homomorphisms are pointed maps. *)
Definition pmap_GroupHomomorphism {G H : Group} (f : GroupHomomorphism G H) : G ->* H
  := Build_pMap f (isunitpreserving_grp_homo f).
Coercion pmap_GroupHomomorphism : GroupHomomorphism >-> pForall.

Definition issig_GroupHomomorphism (G H : Group) : _ <~> GroupHomomorphism G H
  := ltac:(issig).

(** Function extensionality for group homomorphisms. *)
Definition equiv_path_grouphomomorphism {F : Funext} {G H : Group}
  {g h : GroupHomomorphism G H} : g == h <~> g = h.F: Funext
G, H: Group
g, h: GroupHomomorphism G H
g == h <~> g = h
Proof.F: Funext
G, H: Group
g, h: GroupHomomorphism G H
g == h <~> g = h
  refine ((equiv_ap (issig_GroupHomomorphism G H)^-1 _ _)^-1 oE _).F: Funext
G, H: Group
g, h: GroupHomomorphism G H
g == h <~>
(issig_GroupHomomorphism G H)^-1 g =
(issig_GroupHomomorphism G H)^-1 h
  refine (equiv_path_sigma_hprop _ _ oE _).F: Funext
G, H: Group
g, h: GroupHomomorphism G H
g == h <~>
((issig_GroupHomomorphism G H)^-1 g).1 =
((issig_GroupHomomorphism G H)^-1 h).1
  apply equiv_path_forall.
Defined.

(** Group homomorphisms are sets, in the presence of funext. *)
Instance ishset_grouphomomorphism {F : Funext} {G H : Group}
  : IsHSet (GroupHomomorphism G H).F: Funext
G, H: Group
IsHSet (GroupHomomorphism G H)
Proof.F: Funext
G, H: Group
IsHSet (GroupHomomorphism G H)
  apply istrunc_S.F: Funext
G, H: Group
is_mere_relation (GroupHomomorphism G H) paths
  intros f g; exact (istrunc_equiv_istrunc _ equiv_path_grouphomomorphism).
Defined.

(** Group homomorphisms preserve inverses. *)
Definition grp_homo_inv {G H} (f : GroupHomomorphism G H)
  : forall x, f x^ = (f x)^.G, H: Group
f: GroupHomomorphism G H
forall x : G, f x^ = (f x)^
(* This can also be proved using [:= preserves_inverse.] from Classes/theory/groups.v.  That uses [rewrite] and is marked [Qed]. *)
Proof.G, H: Group
f: GroupHomomorphism G H
forall x : G, f x^ = (f x)^
  intro x.G, H: Group
f: GroupHomomorphism G H
x: G
f x^ = (f x)^
  apply (inverse_unique (f x)).G, H: Group
f: GroupHomomorphism G H
x: G
f x^ * f x = 1
G, H: Group
f: GroupHomomorphism G H
x: G
f x * (f x)^ = 1
  +G, H: Group
f: GroupHomomorphism G H
x: G
f x^ * f x = 1 refine (_ @ grp_homo_unit f).G, H: Group
f: GroupHomomorphism G H
x: G
f x^ * f x = f 1
    refine ((grp_homo_op f _ x)^ @ _).G, H: Group
f: GroupHomomorphism G H
x: G
f (x^ * x) = f 1
    apply ap.G, H: Group
f: GroupHomomorphism G H
x: G
x^ * x = 1
    apply grp_inv_l.
  +G, H: Group
f: GroupHomomorphism G H
x: G
f x * (f x)^ = 1 apply grp_inv_r.
Defined.
#[export] Hint Immediate grp_homo_inv : group_db.

(** The identity map is a group homomorphism. *)
Definition grp_homo_id {G : Group} : GroupHomomorphism G G
  := Build_GroupHomomorphism idmap _.

(** The composition of the underlying functions of two group homomorphisms is also a group homomorphism. *)
Definition grp_homo_compose {G H K : Group}
  : GroupHomomorphism H K -> GroupHomomorphism G H -> GroupHomomorphism G K.G, H, K: Group
GroupHomomorphism H K ->
GroupHomomorphism G H -> GroupHomomorphism G K
Proof.G, H, K: Group
GroupHomomorphism H K ->
GroupHomomorphism G H -> GroupHomomorphism G K
  intros f g.G, H, K: Group
f: GroupHomomorphism H K
g: GroupHomomorphism G H
GroupHomomorphism G K
  srapply (Build_GroupHomomorphism (f o g)).
Defined.

(** ** Group Isomorphisms *)

(** Group isomorphisms are group homomorphisms whose underlying map happens to be an equivalence. They allow us to consider two groups to be the "same". They can be inverted and composed just like equivalences. *)

(** An isomorphism of groups is defined as group homomorphism that is an equivalence. *)
Record GroupIsomorphism (G H : Group) := Build_GroupIsomorphism {
  grp_iso_homo :> GroupHomomorphism G H;
  isequiv_group_iso :: IsEquiv grp_iso_homo;
}.

(** We can build an isomorphism from an operation-preserving equivalence. *)
Definition Build_GroupIsomorphism' {G H : Group}
  (f : G <~> H) (h : IsSemiGroupPreserving f)
  : GroupIsomorphism G H.G, H: Group
f: G <~> H
h: IsSemiGroupPreserving f
GroupIsomorphism G H
Proof.G, H: Group
f: G <~> H
h: IsSemiGroupPreserving f
GroupIsomorphism G H
  srapply Build_GroupIsomorphism.G, H: Group
f: G <~> H
h: IsSemiGroupPreserving f
GroupHomomorphism G H
G, H: Group
f: G <~> H
h: IsSemiGroupPreserving f
IsEquiv ?grp_iso_homo
  1: srapply Build_GroupHomomorphism.G, H: Group
f: G <~> H
h: IsSemiGroupPreserving f
IsEquiv
  {|
    grp_homo_map := f;
    issemigrouppreserving_grp_homo := h
  |}
  exact _.
Defined.

Definition issig_GroupIsomorphism (G H : Group)
  : _ <~> GroupIsomorphism G H := ltac:(issig).

(** The underlying equivalence of a group isomorphism. *)
Definition equiv_groupisomorphism {G H : Group}
  : GroupIsomorphism G H -> G <~> H
  := fun f => Build_Equiv G H f _.
Coercion equiv_groupisomorphism : GroupIsomorphism >-> Equiv.

(** The underlying pointed equivalence of a group isomorphism. *)
Definition pequiv_groupisomorphism {A B : Group}
  : GroupIsomorphism A B -> (A <~>* B)
  := fun f => Build_pEquiv f _.
Coercion pequiv_groupisomorphism : GroupIsomorphism >-> pEquiv.

(** Funext for group isomorphisms. *)
Definition equiv_path_groupisomorphism `{F : Funext} {G H : Group}
  (f g : GroupIsomorphism G H)
  : f == g <~> f = g.F: Funext
G, H: Group
f, g: GroupIsomorphism G H
f == g <~> f = g
Proof.F: Funext
G, H: Group
f, g: GroupIsomorphism G H
f == g <~> f = g
  refine ((equiv_ap (issig_GroupIsomorphism G H)^-1 _ _)^-1 oE _).F: Funext
G, H: Group
f, g: GroupIsomorphism G H
f == g <~>
(issig_GroupIsomorphism G H)^-1 f =
(issig_GroupIsomorphism G H)^-1 g
  refine (equiv_path_sigma_hprop _ _ oE _).F: Funext
G, H: Group
f, g: GroupIsomorphism G H
f == g <~>
((issig_GroupIsomorphism G H)^-1 f).1 =
((issig_GroupIsomorphism G H)^-1 g).1
  exact equiv_path_grouphomomorphism.
Defined.

(** Group isomorphisms form a set. *)
Definition ishset_groupisomorphism `{F : Funext} {G H : Group}
  : IsHSet (GroupIsomorphism G H).F: Funext
G, H: Group
IsHSet (GroupIsomorphism G H)
Proof.F: Funext
G, H: Group
IsHSet (GroupIsomorphism G H)
  apply istrunc_S.F: Funext
G, H: Group
is_mere_relation (GroupIsomorphism G H) paths
  intros f g; exact (istrunc_equiv_istrunc _ (equiv_path_groupisomorphism _ _)).
Defined.

(** The identity map is an equivalence and therefore a group isomorphism. *)
Definition grp_iso_id {G : Group} : GroupIsomorphism G G
  := Build_GroupIsomorphism _ _ grp_homo_id _.

(** Group isomorphisms can be composed by composing the underlying group homomorphism. *)
Definition grp_iso_compose {G H K : Group}
  (g : GroupIsomorphism H K) (f : GroupIsomorphism G H)
  : GroupIsomorphism G K
  := Build_GroupIsomorphism _ _ (grp_homo_compose g f) _.

(** Group isomorphisms can be inverted. The inverse map of the underlying equivalence also preserves the group operation and unit. *)
Definition grp_iso_inverse {G H : Group}
  : GroupIsomorphism G H -> GroupIsomorphism H G.G, H: Group
GroupIsomorphism G H -> GroupIsomorphism H G
Proof.G, H: Group
GroupIsomorphism G H -> GroupIsomorphism H G
  intros [f e].G, H: Group
f: GroupHomomorphism G H
e: IsEquiv f
GroupIsomorphism H G
  srapply Build_GroupIsomorphism.G, H: Group
f: GroupHomomorphism G H
e: IsEquiv f
GroupHomomorphism H G
G, H: Group
f: GroupHomomorphism G H
e: IsEquiv f
IsEquiv ?grp_iso_homo
  -G, H: Group
f: GroupHomomorphism G H
e: IsEquiv f
GroupHomomorphism H G srapply (Build_GroupHomomorphism f^-1).
  -G, H: Group
f: GroupHomomorphism G H
e: IsEquiv f
IsEquiv
  {|
    grp_homo_map := f^-1;
    issemigrouppreserving_grp_homo := monmor_sgmor
  |} exact _.
Defined.

(** Group isomorphism is a reflexive relation. *)
Instance reflexive_groupisomorphism
  : Reflexive GroupIsomorphism
  := fun G => grp_iso_id.

(** Group isomorphism is a symmetric relation. *)
Instance symmetric_groupisomorphism
  : Symmetric GroupIsomorphism
  := fun G H => grp_iso_inverse.

(** Group isomorphism is a transitive relation. *)
Instance transitive_groupisomorphism
  : Transitive GroupIsomorphism
  := fun G H K f g => grp_iso_compose g f.

(** Under univalence, equality of groups is equivalent to isomorphism of groups. This is the structure identity principle for groups. *)
Definition equiv_path_group' {U : Univalence} {G H : Group}
  : GroupIsomorphism G H <~> G = H.U: Univalence
G, H: Group
GroupIsomorphism G H <~> G = H
Proof.U: Univalence
G, H: Group
GroupIsomorphism G H <~> G = H
  equiv_via {f : G <~> H & IsSemiGroupPreserving f}.U: Univalence
G, H: Group
GroupIsomorphism G H <~>
{f : G <~> H & IsSemiGroupPreserving f}
U: Univalence
G, H: Group
{f : G <~> H & IsSemiGroupPreserving f} <~> G = H
  1: make_equiv.U: Univalence
G, H: Group
{f : G <~> H & IsSemiGroupPreserving f} <~> G = H
  revert G H; apply (equiv_path_issig_contr issig_group).U: Univalence
forall
b : {H : Type &
    {H0 : SgOp H &
    {H1 : MonUnit H &
    {H2 : Inverse H &
    {_ : IsGroup H & Associative (flip H0)}}}}},
{f : issig_group b <~> issig_group b &
IsSemiGroupPreserving f}
U: Univalence
forall
b1 : {H : Type &
     {H0 : SgOp H &
     {H1 : MonUnit H &
     {H2 : Inverse H &
     {_ : IsGroup H & Associative (flip H0)}}}}},
Contr
  {b2
  : {H : Type &
    {H0 : SgOp H &
    {H1 : MonUnit H &
    {H2 : Inverse H &
    {_ : IsGroup H & Associative (flip H0)}}}}} &
  {f : issig_group b1 <~> issig_group b2 &
  IsSemiGroupPreserving f}}
  -U: Univalence
forall
b : {H : Type &
    {H0 : SgOp H &
    {H1 : MonUnit H &
    {H2 : Inverse H &
    {_ : IsGroup H & Associative (flip H0)}}}}},
{f : issig_group b <~> issig_group b &
IsSemiGroupPreserving f} intros [G [? [? [? ?]]]].U: Univalence
G: Type
proj1: SgOp G
proj0: MonUnit G
proj2: Inverse G
proj3: {_ : IsGroup G & Associative (flip proj1)}
{f
: issig_group (G; proj1; proj0; proj2; proj3) <~>
  issig_group (G; proj1; proj0; proj2; proj3) &
IsSemiGroupPreserving f}
    exists 1%equiv.U: Univalence
G: Type
proj1: SgOp G
proj0: MonUnit G
proj2: Inverse G
proj3: {_ : IsGroup G & Associative (flip proj1)}
IsSemiGroupPreserving 1%equiv
    exact _.
  -U: Univalence
forall
b1 : {H : Type &
     {H0 : SgOp H &
     {H1 : MonUnit H &
     {H2 : Inverse H &
     {_ : IsGroup H & Associative (flip H0)}}}}},
Contr
  {b2
  : {H : Type &
    {H0 : SgOp H &
    {H1 : MonUnit H &
    {H2 : Inverse H &
    {_ : IsGroup H & Associative (flip H0)}}}}} &
  {f : issig_group b1 <~> issig_group b2 &
  IsSemiGroupPreserving f}} intros [G [op [unit [neg [ax assoc_op]]]]]; cbn.U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
Contr
  {b2
  : {H : Type &
    {H0 : SgOp H &
    {H1 : MonUnit H &
    {H2 : Inverse H &
    {_ : IsGroup H & Associative (flip H0)}}}}} &
  {f : G <~> b2.1 & IsSemiGroupPreserving f}}
    contr_sigsig G (equiv_idmap G).U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
Contr
  {y
  : {H0 : SgOp G &
    {H1 : MonUnit G &
    {H2 : Inverse G &
    {_ : IsGroup G & Associative (flip H0)}}}} &
  IsSemiGroupPreserving 1%equiv}
    srefine (Build_Contr _ ((_;(_;(_;(_; _))));_) _); cbn.U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
Associative (flip op)
U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
IsSemiGroupPreserving idmap
U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
forall
y : {y
    : {H0 : SgOp G &
      {H1 : MonUnit G &
      {H2 : Inverse G &
      {_ : IsGroup G & Associative (flip H0)}}}} &
    IsSemiGroupPreserving idmap},
((op; unit; neg; ax; ?Goal); ?Goal0) = y
    1: assumption.U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
IsSemiGroupPreserving idmap
U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
forall
y : {y
    : {H0 : SgOp G &
      {H1 : MonUnit G &
      {H2 : Inverse G &
      {_ : IsGroup G & Associative (flip H0)}}}} &
    IsSemiGroupPreserving idmap},
((op; unit; neg; ax; assoc_op); ?Goal) = y
    1: exact _.U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
forall
y : {y
    : {H0 : SgOp G &
      {H1 : MonUnit G &
      {H2 : Inverse G &
      {_ : IsGroup G & Associative (flip H0)}}}} &
    IsSemiGroupPreserving idmap},
((op; unit; neg; ax; assoc_op);
abstract_algebra.id_sg_morphism) = y
    intros [[op' [unit' [neg' [ax' assoc_op']]]] eq].U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
((op; unit; neg; ax; assoc_op);
abstract_algebra.id_sg_morphism) =
((op'; unit'; neg'; ax'; assoc_op'); eq)
    apply path_sigma_hprop; cbn.U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
(op; unit; neg; ax; assoc_op) =
(op'; unit'; neg'; ax'; assoc_op')
    refine (@ap _ _ (fun x : { oun :
      { oo : SgOp G & { u : MonUnit G & Inverse G}}
      & { _ : @IsGroup G oun.1 oun.2.1 oun.2.2
        & forall z y x, oun.1 (oun.1 x y) z = oun.1 x (oun.1 y z)}}
      => (x.1.1 ; x.1.2.1 ; x.1.2.2 ; (x.2.1; x.2.2)))
      ((op;unit;neg);(ax; assoc_op)) ((op';unit';neg');(ax'; assoc_op')) _).U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
((op; unit; neg); ax; assoc_op) =
((op'; unit'; neg'); ax'; assoc_op')
    apply path_sigma_hprop; cbn.U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
(op; unit; neg) = (op'; unit'; neg')
    srefine (path_sigma' _ _ _).U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
op = op'
U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
transport
  (fun _ : SgOp G => {_ : MonUnit G & Inverse G}) 
  ?p (unit; neg) = (unit'; neg')
    1: funext x y; apply eq.U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
transport
  (fun _ : SgOp G => {_ : MonUnit G & Inverse G})
  (path_forall op op'
     ((fun x : G =>
       path_forall (op x) (op' x)
         ((fun y : G => eq x y) : op x == op' x))
      :
      op == op')) (unit; neg) = (unit'; neg')
    rewrite transport_const.U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
(unit; neg) = (unit'; neg')
    pose (f := Build_GroupHomomorphism
        (G:=Build_Group_internal G op unit neg ax assoc_op)
        (H:=Build_Group_internal G op' unit' neg' ax' assoc_op')
        idmap eq).U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
f:= {|
  grp_homo_map := idmap;
  issemigrouppreserving_grp_homo := eq
|}: GroupHomomorphism
  {|
    group_type := G;
    group_sgop := op;
    group_unit := unit;
    group_inverse := neg;
    group_isgroup := ax;
    group_assoc_opp := assoc_op
  |}
  {|
    group_type := G;
    group_sgop := op';
    group_unit := unit';
    group_inverse := neg';
    group_isgroup := ax';
    group_assoc_opp := assoc_op'
  |}
(unit; neg) = (unit'; neg')
    srefine (path_sigma' _ _ _).U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
f:= {|
  grp_homo_map := idmap;
  issemigrouppreserving_grp_homo := eq
|}: GroupHomomorphism
  {|
    group_type := G;
    group_sgop := op;
    group_unit := unit;
    group_inverse := neg;
    group_isgroup := ax;
    group_assoc_opp := assoc_op
  |}
  {|
    group_type := G;
    group_sgop := op';
    group_unit := unit';
    group_inverse := neg';
    group_isgroup := ax';
    group_assoc_opp := assoc_op'
  |}
unit = unit'
U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
f:= {|
  grp_homo_map := idmap;
  issemigrouppreserving_grp_homo := eq
|}: GroupHomomorphism
  {|
    group_type := G;
    group_sgop := op;
    group_unit := unit;
    group_inverse := neg;
    group_isgroup := ax;
    group_assoc_opp := assoc_op
  |}
  {|
    group_type := G;
    group_sgop := op';
    group_unit := unit';
    group_inverse := neg';
    group_isgroup := ax';
    group_assoc_opp := assoc_op'
  |}
transport (fun _ : MonUnit G => Inverse G) ?p neg =
neg'
    1: exact (grp_homo_unit f).U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
f:= {|
  grp_homo_map := idmap;
  issemigrouppreserving_grp_homo := eq
|}: GroupHomomorphism
  {|
    group_type := G;
    group_sgop := op;
    group_unit := unit;
    group_inverse := neg;
    group_isgroup := ax;
    group_assoc_opp := assoc_op
  |}
  {|
    group_type := G;
    group_sgop := op';
    group_unit := unit';
    group_inverse := neg';
    group_isgroup := ax';
    group_assoc_opp := assoc_op'
  |}
transport (fun _ : MonUnit G => Inverse G)
  (grp_homo_unit f) neg = neg'
    lhs napply transport_const.U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
f:= {|
  grp_homo_map := idmap;
  issemigrouppreserving_grp_homo := eq
|}: GroupHomomorphism
  {|
    group_type := G;
    group_sgop := op;
    group_unit := unit;
    group_inverse := neg;
    group_isgroup := ax;
    group_assoc_opp := assoc_op
  |}
  {|
    group_type := G;
    group_sgop := op';
    group_unit := unit';
    group_inverse := neg';
    group_isgroup := ax';
    group_assoc_opp := assoc_op'
  |}
neg = neg'
    funext x.U: Univalence
G: Type
op: SgOp G
unit: MonUnit G
neg: Inverse G
ax: IsGroup G
assoc_op: Associative (flip op)
op': SgOp G
unit': MonUnit G
neg': Inverse G
ax': IsGroup G
assoc_op': Associative (flip op')
eq: IsSemiGroupPreserving idmap
f:= {|
  grp_homo_map := idmap;
  issemigrouppreserving_grp_homo := eq
|}: GroupHomomorphism
  {|
    group_type := G;
    group_sgop := op;
    group_unit := unit;
    group_inverse := neg;
    group_isgroup := ax;
    group_assoc_opp := assoc_op
  |}
  {|
    group_type := G;
    group_sgop := op';
    group_unit := unit';
    group_inverse := neg';
    group_isgroup := ax';
    group_assoc_opp := assoc_op'
  |}
x: G
neg x = neg' x
    exact (grp_homo_inv f x).
Defined.

(** A version with nicer universe variables. *)
Definition equiv_path_group@{u v | u < v} {U : Univalence} {G H : Group@{u}}
  : GroupIsomorphism G H <~> (paths@{v} G H)
  := equiv_path_group'.

(** ** Simple group equivalences *)

(** Left multiplication is an equivalence. *)
Instance isequiv_group_left_op {G : Group}
  : forall (x : G), IsEquiv (x *.).G: Group
forall x : G, IsEquiv (sg_op x)
Proof.G: Group
forall x : G, IsEquiv (sg_op x)
  intro x.G: Group
x: G
IsEquiv (sg_op x)
  srapply isequiv_adjointify.G: Group
x: G
G -> G
G: Group
x: G
sg_op x o ?g == idmap
G: Group
x: G
?g o sg_op x == idmap
  1: exact (x^ *.).G: Group
x: G
sg_op x o sg_op x^ == idmap
G: Group
x: G
sg_op x^ o sg_op x == idmap
  all: intro y.G: Group
x, y: G
x * (x^ * y) = y
G: Group
x, y: G
x^ * (x * y) = y
  all: refine (grp_assoc _ _ _ @ _ @ grp_unit_l y).G: Group
x, y: G
x * x^ * y = 1 * y
G: Group
x, y: G
x^ * x * y = 1 * y
  all: refine (ap (fun x => x * y) _).G: Group
x, y: G
x * x^ = 1
G: Group
x, y: G
x^ * x = 1
  1: apply grp_inv_r.G: Group
x, y: G
x^ * x = 1
  apply grp_inv_l.
Defined.

(** Right multiplication is an equivalence. *)
Instance isequiv_group_right_op (G : Group)
  : forall (x : G), IsEquiv (fun y => y * x).G: Group
forall x : G, IsEquiv (fun y : G => y * x)
Proof.G: Group
forall x : G, IsEquiv (fun y : G => y * x)
  intro x.G: Group
x: G
IsEquiv (fun y : G => y * x)
  srapply isequiv_adjointify.G: Group
x: G
G -> G
G: Group
x: G
(fun y : G => y * x) o ?g == idmap
G: Group
x: G
?g o (fun y : G => y * x) == idmap
  1: exact (fun y => y * x^).G: Group
x: G
(fun y : G => y * x) o (fun y : G => y * x^) == idmap
G: Group
x: G
(fun y : G => y * x^) o (fun y : G => y * x) == idmap
  all: intro y.G: Group
x, y: G
y * x^ * x = y
G: Group
x, y: G
y * x * x^ = y
  all: refine ((grp_assoc _ _ _)^ @ _ @ grp_unit_r y).G: Group
x, y: G
y * (x^ * x) = y * 1
G: Group
x, y: G
y * (x * x^) = y * 1
  all: refine (ap (y *.) _).G: Group
x, y: G
x^ * x = 1
G: Group
x, y: G
x * x^ = 1
  1: apply grp_inv_l.G: Group
x, y: G
x * x^ = 1
  apply grp_inv_r.
Defined.

(** The operation inverting group elements is an equivalence. Note that, since the order of the operation will change after inversion, this isn't a group homomorphism. *)
Instance isequiv_group_inverse {G : Group}
  : IsEquiv ((^) : G -> G).G: Group
IsEquiv (inv : G -> G)
Proof.G: Group
IsEquiv (inv : G -> G)
  srapply isequiv_involution.G: Group
inv o inv == idmap
  exact inverse_involutive.
Defined.

(** ** Reasoning with equations in groups. *)

Section GroupEquations.

  Context {G : Group} (x y z : G).

  (** Inverses are involutive. *)
  Definition grp_inv_inv : x^^ = x := inverse_involutive x.

  (** Inverses distribute over the group operation. *)
  Definition grp_inv_op : (x * y)^ = y^ * x^ := inverse_sg_op x y.

  (** The inverse of the unit is the unit. *)
  Definition grp_inv_unit : mon_unit^ = mon_unit := inverse_mon_unit (G :=G).

  Definition grp_inv_V_gg : x^ * (x * y) = y
    := grp_assoc _ _ _ @ ap (.* y) (grp_inv_l x) @ grp_unit_l y.

  Definition grp_inv_g_Vg : x * (x^ * y) = y
    := grp_assoc _ _ _ @ ap (.* y) (grp_inv_r x) @ grp_unit_l y.

  Definition grp_inv_gg_V : (x * y) * y^ = x
    := (grp_assoc _ _ _)^ @ ap (x *.) (grp_inv_r y) @ grp_unit_r x.

  Definition grp_inv_gV_g : (x * y^) * y = x
    := (grp_assoc _ _ _)^ @ ap (x *.) (grp_inv_l y) @ grp_unit_r x.

  Definition grp_1g_g1 : x = y <~> 1 * x = y * 1
    := equiv_concat_r (grp_unit_r _)^ _ oE equiv_concat_l (grp_unit_l _) _.

  Definition grp_g1_1g : x = y <~> x * 1 = 1 * y
    := equiv_concat_r (grp_unit_l _)^ _ oE equiv_concat_l (grp_unit_r _) _.

End GroupEquations.

(** ** Cancellation lemmas *)

(** Group elements can be cancelled both on the left and the right. *)
Definition grp_cancelL {G : Group} {x y : G} z : x = y <~> z * x = z * y
  := equiv_ap (fun x => z * x) _ _.
Definition grp_cancelR {G : Group} {x y : G} z : x = y <~> x * z = y * z
  := equiv_ap (fun x => x * z) _ _.

(** ** Group movement lemmas *)

Section GroupMovement.

  (** Since left/right multiplication is an equivalence, we can use lemmas about moving equivalences around to prove group movement lemmas. *)

  Context {G : Group} {x y z : G}.

  (** *** Moving group elements *)

  Definition grp_moveL_gM : x * z^ = y <~> x = y * z
    := equiv_moveL_equiv_M (f := fun t => t * z) _ _.

  Definition grp_moveL_Mg : y^ * x = z <~> x = y * z
    := equiv_moveL_equiv_M (f := fun t => y * t) _ _.

  Definition grp_moveR_gM : x = z * y^ <~> x * y = z
    := equiv_moveR_equiv_M (f := fun t => t * y) _ _.

  Definition grp_moveR_Mg : y = x^ * z <~> x * y = z
    := equiv_moveR_equiv_M (f := fun t => x * t) _ _.

  (** *** Moving inverses.*)
  (** These are the inverses of the previous but are included here for completeness*)
  Definition grp_moveR_gV : x = y * z <~> x * z^ = y
    := equiv_moveR_equiv_V (f := fun t => t * z) _ _.

  Definition grp_moveR_Vg : x = y * z <~> y^ * x = z
    := equiv_moveR_equiv_V (f := fun t => y * t) _ _.

  Definition grp_moveL_gV :  x * y = z <~> x = z * y^
    := equiv_moveL_equiv_V (f := fun t => t * y) _ _.

  Definition grp_moveL_Vg :  x * y = z <~> y = x^ * z
    := equiv_moveL_equiv_V (f := fun t => x * t) _ _.

(** We close the section here so the previous lemmas generalise their assumptions. *)
End GroupMovement.

Section GroupMovement.

  Context {G : Group} {x y z : G}.

  (** *** Moving elements equal to unit. *)

  Definition grp_moveL_1M : x * y^ = 1 <~> x = y
    := equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gM.

  Definition grp_moveL_M1 : y^ * x = 1 <~> x = y
    := equiv_concat_r (grp_unit_r _) _ oE grp_moveL_Mg.

  Definition grp_moveL_1V : x * y = 1 <~> x = y^
    := equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gV.

  Definition grp_moveL_V1 : y * x = 1 <~> x = y^
    := equiv_concat_r (grp_unit_r _) _ oE grp_moveL_Vg.

  Definition grp_moveR_1M : 1 = y * x^ <~> x = y
    := (equiv_concat_l (grp_unit_l _) _)^-1 oE grp_moveR_gM.

  Definition grp_moveR_M1 : 1 = x^ * y <~> x = y
    := (equiv_concat_l (grp_unit_r _) _)^-1 oE grp_moveR_Mg.

  Definition grp_moveR_1V : 1 = y * x <~> x^ = y
    := (equiv_concat_l (grp_unit_l _) _)^-1 oE grp_moveR_gV.

  Definition grp_moveR_V1 : mon_unit = x * y <~> x^ = y
    := (equiv_concat_l (grp_unit_r _) _)^-1 oE grp_moveR_Vg.

  (** *** Cancelling elements equal to unit. *)

  Definition grp_cancelL1 : x = mon_unit <~> z * x = z
    := (equiv_concat_r (grp_unit_r _) _ oE grp_cancelL z).

  Definition grp_cancelR1 : x = mon_unit <~> x * z = z
    := (equiv_concat_r (grp_unit_l _) _) oE grp_cancelR z.

End GroupMovement.

(** ** Commutation *)

(** If [g] commutes with [h], then [g] commutes with the inverse [-h]. *)
Definition grp_commutes_inv {G : Group} (g h : G) (p : g * h = h * g)
  : g * h^ = h^ * g.G: Group
g, h: G
p: g * h = h * g
g * h^ = h^ * g
Proof.G: Group
g, h: G
p: g * h = h * g
g * h^ = h^ * g
  apply grp_moveR_gV.G: Group
g, h: G
p: g * h = h * g
g = h^ * g * h
  rhs_V apply simple_associativity.G: Group
g, h: G
p: g * h = h * g
g = h^ * (g * h)
  by apply grp_moveL_Vg.
Defined.

(** If [g] commutes with [h] and [h'], then [g] commutes with their product [h * h']. *)
Definition grp_commutes_op {G : Group} (g h h' : G)
  (p : g * h = h * g) (p' : g * h' = h' * g)
  : g * (h * h') = (h * h') * g.G: Group
g, h, h': G
p: g * h = h * g
p': g * h' = h' * g
g * (h * h') = h * h' * g
Proof.G: Group
g, h, h': G
p: g * h = h * g
p': g * h' = h' * g
g * (h * h') = h * h' * g
  lhs apply simple_associativity.G: Group
g, h, h': G
p: g * h = h * g
p': g * h' = h' * g
g * h * h' = h * h' * g
  lhs exact (ap (.* h') p).G: Group
g, h, h': G
p: g * h = h * g
p': g * h' = h' * g
h * g * h' = h * h' * g
  lhs_V apply simple_associativity.G: Group
g, h, h': G
p: g * h = h * g
p': g * h' = h' * g
h * (g * h') = h * h' * g
  lhs exact (ap (h *.) p').G: Group
g, h, h': G
p: g * h = h * g
p': g * h' = h' * g
h * (h' * g) = h * h' * g
  by apply simple_associativity.
Defined.

(** ** Power operation *)

(** For a given [g : G] we can define the function [Int -> G] sending an integer to that power of [g]. *)
Definition grp_pow {G : Group} (g : G) (n : Int) : G
  := int_iter (g *.) n mon_unit.

(** Any homomorphism respects [grp_pow]. In other words, [fun g => grp_pow g n] is natural. *)
Lemma grp_pow_natural {G H : Group} (f : GroupHomomorphism G H) (n : Int) (g : G)
  : f (grp_pow g n) = grp_pow (f g) n.G, H: Group
f: GroupHomomorphism G H
n: Int
g: G
f (grp_pow g n) = grp_pow (f g) n
Proof.G, H: Group
f: GroupHomomorphism G H
n: Int
g: G
f (grp_pow g n) = grp_pow (f g) n
  lhs snapply (int_iter_commute_map _ ((f g) *.)).G, H: Group
f: GroupHomomorphism G H
n: Int
g: G
(fun x : G => f (g * x)) == (fun x : G => f g * f x)
G, H: Group
f: GroupHomomorphism G H
n: Int
g: G
int_iter (sg_op (f g)) n (f 1) = grp_pow (f g) n
  1: napply grp_homo_op.G, H: Group
f: GroupHomomorphism G H
n: Int
g: G
int_iter (sg_op (f g)) n (f 1) = grp_pow (f g) n
  apply (ap (int_iter _ n)), grp_homo_unit.
Defined.

(** All powers of the unit are the unit. *)
Definition grp_pow_unit {G : Group} (n : Int)
  : grp_pow (G:=G) mon_unit n = mon_unit.G: Group
n: Int
grp_pow 1 n = 1
Proof.G: Group
n: Int
grp_pow 1 n = 1
  snapply (int_iter_invariant n _ (fun g => g = mon_unit)); cbn.G: Group
n: Int
forall x : G, x = 1 -> 1 * x = 1
G: Group
n: Int
forall x : G, x = 1 -> 1^ * x = 1
G: Group
n: Int
1 = 1
  1, 2: apply paths_ind_r.G: Group
n: Int
1 * 1 = 1
G: Group
n: Int
1^ * 1 = 1
G: Group
n: Int
1 = 1
  -G: Group
n: Int
1 * 1 = 1 apply grp_unit_r.
  -G: Group
n: Int
1^ * 1 = 1 lhs napply grp_unit_r.G: Group
n: Int
1^ = 1 exact grp_inv_unit.
  -G: Group
n: Int
1 = 1 reflexivity.
Defined.

(** Note that powers don't preserve the group operation as it is not commutative. This does hold in an abelian group so such a result will appear later. *)

(** The next two results tell us how [grp_pow] unfolds. *)
Definition grp_pow_succ {G : Group} (n : Int) (g : G)
  : grp_pow g (n.+1)%int = g * grp_pow g n
  := int_iter_succ_l _ _ _.

Definition grp_pow_pred {G : Group} (n : Int) (g : G)
  : grp_pow g (n.-1)%int = g^ * grp_pow g n
  := int_iter_pred_l _ _ _.

(** [grp_pow] satisfies an additive law of exponents. *)
Definition grp_pow_add {G : Group} (m n : Int) (g : G)
  : grp_pow g (n + m)%int = grp_pow g n * grp_pow g m.G: Group
m, n: Int
g: G
grp_pow g (n + m)%int = grp_pow g n * grp_pow g m
Proof.G: Group
m, n: Int
g: G
grp_pow g (n + m)%int = grp_pow g n * grp_pow g m
  lhs napply int_iter_add.G: Group
m, n: Int
g: G
int_iter (sg_op g) n (int_iter (sg_op g) m 1) =
grp_pow g n * grp_pow g m
  induction n; cbn.G: Group
m: Int
g: G
int_iter (sg_op g) m 1 = 1 * grp_pow g m
G: Group
m: Int
n: nat
g: G
IHn: int_iter (sg_op g) n (int_iter (sg_op g) m 1) = grp_pow g n * grp_pow g m
int_iter (sg_op g) n.+1%int (int_iter (sg_op g) m 1) =
grp_pow g n.+1%int * grp_pow g m
G: Group
m: Int
n: nat
g: G
IHn: int_iter (sg_op g) (- n)%int (int_iter (sg_op g) m 1) =
grp_pow g (- n)%int * grp_pow g m
int_iter (sg_op g) (- n).-1%int
  (int_iter (sg_op g) m 1) =
grp_pow g (- n).-1%int * grp_pow g m
  1: symmetry; exact (grp_unit_l _).G: Group
m: Int
n: nat
g: G
IHn: int_iter (sg_op g) n (int_iter (sg_op g) m 1) = grp_pow g n * grp_pow g m
int_iter (sg_op g) n.+1%int (int_iter (sg_op g) m 1) =
grp_pow g n.+1%int * grp_pow g m
G: Group
m: Int
n: nat
g: G
IHn: int_iter (sg_op g) (- n)%int (int_iter (sg_op g) m 1) =
grp_pow g (- n)%int * grp_pow g m
int_iter (sg_op g) (- n).-1%int
  (int_iter (sg_op g) m 1) =
grp_pow g (- n).-1%int * grp_pow g m
  1: rewrite int_iter_succ_l, grp_pow_succ.G: Group
m: Int
n: nat
g: G
IHn: int_iter (sg_op g) n (int_iter (sg_op g) m 1) = grp_pow g n * grp_pow g m
g * int_iter (sg_op g) n (int_iter (sg_op g) m 1) =
g * grp_pow g n * grp_pow g m
G: Group
m: Int
n: nat
g: G
IHn: int_iter (sg_op g) (- n)%int (int_iter (sg_op g) m 1) =
grp_pow g (- n)%int * grp_pow g m
int_iter (sg_op g) (- n).-1%int
  (int_iter (sg_op g) m 1) =
grp_pow g (- n).-1%int * grp_pow g m
  2: rewrite int_iter_pred_l, grp_pow_pred; cbn.G: Group
m: Int
n: nat
g: G
IHn: int_iter (sg_op g) n (int_iter (sg_op g) m 1) = grp_pow g n * grp_pow g m
g * int_iter (sg_op g) n (int_iter (sg_op g) m 1) =
g * grp_pow g n * grp_pow g m
G: Group
m: Int
n: nat
g: G
IHn: int_iter (sg_op g) (- n)%int (int_iter (sg_op g) m 1) =
grp_pow g (- n)%int * grp_pow g m
g^ *
int_iter (sg_op g) (- n)%int (int_iter (sg_op g) m 1) =
g^ * grp_pow g (- n)%int * grp_pow g m
  1,2 : rhs_V srapply associativity;
        apply ap, IHn.
Defined.

(** [grp_pow] commutes negative exponents to powers of the inverse *)
Definition grp_pow_neg {G : Group} (n : Int) (g : G)
  : grp_pow g (int_neg n) = grp_pow g^ n.G: Group
n: Int
g: G
grp_pow g (- n)%int = grp_pow g^ n
Proof.G: Group
n: Int
g: G
grp_pow g (- n)%int = grp_pow g^ n
  lhs napply int_iter_neg.G: Group
n: Int
g: G
int_iter (sg_op g)^-1 n 1 = grp_pow g^ n
  cbn; unfold grp_pow.G: Group
n: Int
g: G
int_iter (sg_op g^) n 1 = int_iter (sg_op g^) n 1
  (* These agree, except for the proofs that [sg_op g^] is an equivalence. *)
  apply int_iter_agree.
Defined.

(** Using a negative power in [grp_pow] is the same as first using a positive power and then inverting the result. *)
Definition grp_pow_neg_inv {G: Group} (m : Int) (g : G)
  : grp_pow g (- m)%int = (grp_pow g m)^.G: Group
m: Int
g: G
grp_pow g (- m)%int = (grp_pow g m)^
Proof.G: Group
m: Int
g: G
grp_pow g (- m)%int = (grp_pow g m)^
  apply grp_moveL_1V.G: Group
m: Int
g: G
grp_pow g (- m)%int * grp_pow g m = 1
  lhs_V napply grp_pow_add.G: Group
m: Int
g: G
grp_pow g (- m + m)%int = 1
  by rewrite int_add_neg_l.
Defined.

(** Combining the two previous results gives that a power of an inverse is the inverse of the power. *)
Definition grp_pow_neg_inv' {G: Group} (n: Int) (g : G)
  : grp_pow g^ n = (grp_pow g n)^.G: Group
n: Int
g: G
grp_pow g^ n = (grp_pow g n)^
Proof.G: Group
n: Int
g: G
grp_pow g^ n = (grp_pow g n)^
  lhs_V napply grp_pow_neg.G: Group
n: Int
g: G
grp_pow g (- n)%int = (grp_pow g n)^
  apply grp_pow_neg_inv.
Defined.

(** [grp_pow] satisfies a multiplicative law of exponents. *)
Definition grp_pow_int_mul {G : Group} (m n : Int) (g : G)
  : grp_pow g (m * n)%int = grp_pow (grp_pow g m) n.G: Group
m, n: Int
g: G
grp_pow g (m * n)%int = grp_pow (grp_pow g m) n
Proof.G: Group
m, n: Int
g: G
grp_pow g (m * n)%int = grp_pow (grp_pow g m) n
  induction n.G: Group
m: Int
g: G
grp_pow g (m * 0)%int = grp_pow (grp_pow g m) 0%int
G: Group
m: Int
n: nat
g: G
IHn: grp_pow g (m * n)%int = grp_pow (grp_pow g m) n
grp_pow g (m * n.+1)%int =
grp_pow (grp_pow g m) n.+1%int
G: Group
m: Int
n: nat
g: G
IHn: grp_pow g (m * - n)%int = grp_pow (grp_pow g m) (- n)%int
grp_pow g (m * (- n).-1)%int =
grp_pow (grp_pow g m) (- n).-1%int
  -G: Group
m: Int
g: G
grp_pow g (m * 0)%int = grp_pow (grp_pow g m) 0%int simpl.G: Group
m: Int
g: G
grp_pow g (m * 0)%int = 1
    by rewrite int_mul_0_r.
  -G: Group
m: Int
n: nat
g: G
IHn: grp_pow g (m * n)%int = grp_pow (grp_pow g m) n
grp_pow g (m * n.+1)%int =
grp_pow (grp_pow g m) n.+1%int rewrite int_mul_succ_r.G: Group
m: Int
n: nat
g: G
IHn: grp_pow g (m * n)%int = grp_pow (grp_pow g m) n
grp_pow g (m + m * n)%int =
grp_pow (grp_pow g m) n.+1%int
    rewrite grp_pow_add.G: Group
m: Int
n: nat
g: G
IHn: grp_pow g (m * n)%int = grp_pow (grp_pow g m) n
grp_pow g m * grp_pow g (m * n)%int =
grp_pow (grp_pow g m) n.+1%int
    rewrite grp_pow_succ.G: Group
m: Int
n: nat
g: G
IHn: grp_pow g (m * n)%int = grp_pow (grp_pow g m) n
grp_pow g m * grp_pow g (m * n)%int =
grp_pow g m * grp_pow (grp_pow g m) n
    apply grp_cancelL, IHn.
  -G: Group
m: Int
n: nat
g: G
IHn: grp_pow g (m * - n)%int = grp_pow (grp_pow g m) (- n)%int
grp_pow g (m * (- n).-1)%int =
grp_pow (grp_pow g m) (- n).-1%int rewrite int_mul_pred_r.G: Group
m: Int
n: nat
g: G
IHn: grp_pow g (m * - n)%int = grp_pow (grp_pow g m) (- n)%int
grp_pow g (- m + m * - n)%int =
grp_pow (grp_pow g m) (- n).-1%int
    rewrite grp_pow_add.G: Group
m: Int
n: nat
g: G
IHn: grp_pow g (m * - n)%int = grp_pow (grp_pow g m) (- n)%int
grp_pow g (- m)%int * grp_pow g (m * - n)%int =
grp_pow (grp_pow g m) (- n).-1%int
    rewrite grp_pow_neg_inv.G: Group
m: Int
n: nat
g: G
IHn: grp_pow g (m * - n)%int = grp_pow (grp_pow g m) (- n)%int
(grp_pow g m)^ * grp_pow g (m * - n)%int =
grp_pow (grp_pow g m) (- n).-1%int
    rewrite grp_pow_pred.G: Group
m: Int
n: nat
g: G
IHn: grp_pow g (m * - n)%int = grp_pow (grp_pow g m) (- n)%int
(grp_pow g m)^ * grp_pow g (m * - n)%int =
(grp_pow g m)^ * grp_pow (grp_pow g m) (- n)%int
    apply grp_cancelL, IHn.
Defined.

(** If [h] commutes with [g], then [h] commutes with [grp_pow g n]. *)
Definition grp_pow_commutes {G : Group} (n : Int) (g h : G)
  (p : h * g = g * h)
  : h * (grp_pow g n) = (grp_pow g n) * h.G: Group
n: Int
g, h: G
p: h * g = g * h
h * grp_pow g n = grp_pow g n * h
Proof.G: Group
n: Int
g, h: G
p: h * g = g * h
h * grp_pow g n = grp_pow g n * h
  induction n.G: Group
g, h: G
p: h * g = g * h
h * grp_pow g 0%int = grp_pow g 0%int * h
G: Group
n: nat
g, h: G
p: h * g = g * h
IHn: h * grp_pow g n = grp_pow g n * h
h * grp_pow g n.+1%int = grp_pow g n.+1%int * h
G: Group
n: nat
g, h: G
p: h * g = g * h
IHn: h * grp_pow g (- n)%int = grp_pow g (- n)%int * h
h * grp_pow g (- n).-1%int =
grp_pow g (- n).-1%int * h
  -G: Group
g, h: G
p: h * g = g * h
h * grp_pow g 0%int = grp_pow g 0%int * h by apply grp_g1_1g.
  -G: Group
n: nat
g, h: G
p: h * g = g * h
IHn: h * grp_pow g n = grp_pow g n * h
h * grp_pow g n.+1%int = grp_pow g n.+1%int * h rewrite grp_pow_succ.G: Group
n: nat
g, h: G
p: h * g = g * h
IHn: h * grp_pow g n = grp_pow g n * h
h * (g * grp_pow g n) = g * grp_pow g n * h
    napply grp_commutes_op; assumption.
  -G: Group
n: nat
g, h: G
p: h * g = g * h
IHn: h * grp_pow g (- n)%int = grp_pow g (- n)%int * h
h * grp_pow g (- n).-1%int =
grp_pow g (- n).-1%int * h rewrite grp_pow_pred.G: Group
n: nat
g, h: G
p: h * g = g * h
IHn: h * grp_pow g (- n)%int = grp_pow g (- n)%int * h
h * (g^ * grp_pow g (- n)%int) =
g^ * grp_pow g (- n)%int * h
    napply grp_commutes_op.G: Group
n: nat
g, h: G
p: h * g = g * h
IHn: h * grp_pow g (- n)%int = grp_pow g (- n)%int * h
h * g^ = g^ * h
G: Group
n: nat
g, h: G
p: h * g = g * h
IHn: h * grp_pow g (- n)%int = grp_pow g (- n)%int * h
h * grp_pow g (- n)%int = grp_pow g (- n)%int * h
    2: assumption.G: Group
n: nat
g, h: G
p: h * g = g * h
IHn: h * grp_pow g (- n)%int = grp_pow g (- n)%int * h
h * g^ = g^ * h
    apply grp_commutes_inv, p.
Defined.

(** [grp_pow g n] commutes with [g]. *)
Definition grp_pow_commutes' {G : Group} (n : Int) (g : G)
  : g * grp_pow g n = grp_pow g n * g.G: Group
n: Int
g: G
g * grp_pow g n = grp_pow g n * g
Proof.G: Group
n: Int
g: G
g * grp_pow g n = grp_pow g n * g
  by apply grp_pow_commutes.
Defined.

(** If [g] and [h] commute, then [grp_pow (g * h) n] = (grp_pow g n) * (grp_pow h n)]. *)
Definition grp_pow_mul {G : Group} (n : Int) (g h : G)
  (c : g * h = h * g)
  : grp_pow (g * h) n = (grp_pow g n) * (grp_pow h n).G: Group
n: Int
g, h: G
c: g * h = h * g
grp_pow (g * h) n = grp_pow g n * grp_pow h n
Proof.G: Group
n: Int
g, h: G
c: g * h = h * g
grp_pow (g * h) n = grp_pow g n * grp_pow h n
  induction n.G: Group
g, h: G
c: g * h = h * g
grp_pow (g * h) 0%int =
grp_pow g 0%int * grp_pow h 0%int
G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) n = grp_pow g n * grp_pow h n
grp_pow (g * h) n.+1%int =
grp_pow g n.+1%int * grp_pow h n.+1%int
G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) (- n)%int = grp_pow g (- n)%int * grp_pow h (- n)%int
grp_pow (g * h) (- n).-1%int =
grp_pow g (- n).-1%int * grp_pow h (- n).-1%int
  -G: Group
g, h: G
c: g * h = h * g
grp_pow (g * h) 0%int =
grp_pow g 0%int * grp_pow h 0%int simpl.G: Group
g, h: G
c: g * h = h * g
1 = 1 * 1
    symmetry; napply grp_unit_r.
  -G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) n = grp_pow g n * grp_pow h n
grp_pow (g * h) n.+1%int =
grp_pow g n.+1%int * grp_pow h n.+1%int rewrite 3 grp_pow_succ.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) n = grp_pow g n * grp_pow h n
g * h * grp_pow (g * h) n =
g * grp_pow g n * (h * grp_pow h n)
    rewrite IHn.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) n = grp_pow g n * grp_pow h n
g * h * (grp_pow g n * grp_pow h n) =
g * grp_pow g n * (h * grp_pow h n)
    rewrite 2 grp_assoc.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) n = grp_pow g n * grp_pow h n
g * h * grp_pow g n * grp_pow h n =
g * grp_pow g n * h * grp_pow h n
    apply grp_cancelR.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) n = grp_pow g n * grp_pow h n
g * h * grp_pow g n = g * grp_pow g n * h
    rewrite <- 2 grp_assoc.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) n = grp_pow g n * grp_pow h n
g * (h * grp_pow g n) = g * (grp_pow g n * h)
    apply grp_cancelL.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) n = grp_pow g n * grp_pow h n
h * grp_pow g n = grp_pow g n * h
    apply grp_pow_commutes.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) n = grp_pow g n * grp_pow h n
h * g = g * h
    exact c^%path.
  -G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) (- n)%int = grp_pow g (- n)%int * grp_pow h (- n)%int
grp_pow (g * h) (- n).-1%int =
grp_pow g (- n).-1%int * grp_pow h (- n).-1%int simpl.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) (- n)%int = grp_pow g (- n)%int * grp_pow h (- n)%int
grp_pow (g * h) (- n).-1%int =
grp_pow g (- n).-1%int * grp_pow h (- n).-1%int
    rewrite 3 grp_pow_pred.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) (- n)%int = grp_pow g (- n)%int * grp_pow h (- n)%int
(g * h)^ * grp_pow (g * h) (- n)%int =
g^ * grp_pow g (- n)%int * (h^ * grp_pow h (- n)%int)
    rewrite IHn.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) (- n)%int = grp_pow g (- n)%int * grp_pow h (- n)%int
(g * h)^ * (grp_pow g (- n)%int * grp_pow h (- n)%int) =
g^ * grp_pow g (- n)%int * (h^ * grp_pow h (- n)%int)
    rewrite 2 grp_assoc.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) (- n)%int = grp_pow g (- n)%int * grp_pow h (- n)%int
(g * h)^ * grp_pow g (- n)%int * grp_pow h (- n)%int =
g^ * grp_pow g (- n)%int * h^ * grp_pow h (- n)%int
    apply grp_cancelR.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) (- n)%int = grp_pow g (- n)%int * grp_pow h (- n)%int
(g * h)^ * grp_pow g (- n)%int =
g^ * grp_pow g (- n)%int * h^
    rewrite c.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) (- n)%int = grp_pow g (- n)%int * grp_pow h (- n)%int
(h * g)^ * grp_pow g (- n)%int =
g^ * grp_pow g (- n)%int * h^
    rewrite grp_inv_op.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) (- n)%int = grp_pow g (- n)%int * grp_pow h (- n)%int
g^ * h^ * grp_pow g (- n)%int =
g^ * grp_pow g (- n)%int * h^
    rewrite <- 2 grp_assoc.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) (- n)%int = grp_pow g (- n)%int * grp_pow h (- n)%int
g^ * (h^ * grp_pow g (- n)%int) =
g^ * (grp_pow g (- n)%int * h^)
    apply grp_cancelL.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) (- n)%int = grp_pow g (- n)%int * grp_pow h (- n)%int
h^ * grp_pow g (- n)%int = grp_pow g (- n)%int * h^
    apply grp_pow_commutes.G: Group
n: nat
g, h: G
c: g * h = h * g
IHn: grp_pow (g * h) (- n)%int = grp_pow g (- n)%int * grp_pow h (- n)%int
h^ * g = g * h^
    symmetry; apply grp_commutes_inv, c.
Defined.

(** ** The category of Groups *)

(** ** Groups together with homomorphisms form a 1-category whose equivalences are the group isomorphisms. *)

Instance isgraph_group : IsGraph Group
  := Build_IsGraph Group GroupHomomorphism.

(** We add this coercion to make it easier to use a group isomorphism where Coq expects a category morphism. *)
Definition isHom_GroupIsomorphism (G H : Group) : GroupIsomorphism G H -> Hom G H := idmap.
Coercion isHom_GroupIsomorphism  : GroupIsomorphism >-> Hom.

Instance is01cat_group : Is01Cat Group :=
  Build_Is01Cat Group _ (@grp_homo_id) (@grp_homo_compose).

(** Helper notation so that the wildcat instances can easily be inferred. *)
Local Notation grp_homo_map' A B := (@grp_homo_map A B : _ -> (group_type A $-> _)).

Instance is2graph_group : Is2Graph Group
  := fun A B => isgraph_induced (grp_homo_map' A B).

Instance isgraph_grouphomomorphism {A B : Group} : IsGraph (A $-> B)
  := isgraph_induced (grp_homo_map' A B).

Instance is01cat_grouphomomorphism {A B : Group} : Is01Cat (A $-> B)
  := is01cat_induced (grp_homo_map' A B).

Instance is0gpd_grouphomomorphism {A B : Group}: Is0Gpd (A $-> B)
  := is0gpd_induced (grp_homo_map' A B).

Instance is0functor_postcomp_grouphomomorphism {A B C : Group} (h : B $-> C)
  : Is0Functor (@cat_postcomp Group _ _ A B C h).A, B, C: Group
h: B $-> C
Is0Functor (cat_postcomp A h)
Proof.A, B, C: Group
h: B $-> C
Is0Functor (cat_postcomp A h)
  apply Build_Is0Functor.A, B, C: Group
h: B $-> C
forall a b : A $-> B,
(a $-> b) -> cat_postcomp A h a $-> cat_postcomp A h b
  intros f g p a ; exact (ap h (p a)).
Defined.

Instance is0functor_precomp_grouphomomorphism
       {A B C : Group} (h : A $-> B)
  : Is0Functor (@cat_precomp Group _ _ A B C h).A, B, C: Group
h: A $-> B
Is0Functor (cat_precomp C h)
Proof.A, B, C: Group
h: A $-> B
Is0Functor (cat_precomp C h)
  apply Build_Is0Functor.A, B, C: Group
h: A $-> B
forall a b : B $-> C,
(a $-> b) -> cat_precomp C h a $-> cat_precomp C h b
  intros [f ?] [g ?] p a ; exact (p (h a)).
Defined.

(** Group forms a 1Cat *)
Instance is1cat_group : Is1Cat Group.Is1Cat Group
Proof.Is1Cat Group
  by rapply Build_Is1Cat.
Defined.

(** Under [Funext], the category of groups has morphism extensionality. *)
Instance hasmorext_group `{Funext} : HasMorExt Group.H: Funext
HasMorExt Group
Proof.H: Funext
HasMorExt Group
  intros A B f g; cbn in *.H: Funext
A, B: Group
f, g: GroupHomomorphism A B
IsEquiv GpdHom_path
  snapply @isequiv_homotopic.H: Funext
A, B: Group
f, g: GroupHomomorphism A B
f = g -> f == g
H: Funext
A, B: Group
f, g: GroupHomomorphism A B
IsEquiv ?f
H: Funext
A, B: Group
f, g: GroupHomomorphism A B
?f == GpdHom_path
  1: exact (equiv_path_grouphomomorphism^-1%equiv).H: Funext
A, B: Group
f, g: GroupHomomorphism A B
IsEquiv equiv_path_grouphomomorphism^-1%equiv
H: Funext
A, B: Group
f, g: GroupHomomorphism A B
equiv_path_grouphomomorphism^-1%equiv == GpdHom_path
  1: exact _.H: Funext
A, B: Group
f, g: GroupHomomorphism A B
equiv_path_grouphomomorphism^-1%equiv == GpdHom_path
  intros []; reflexivity. 
Defined.

(** Group isomorphisms become equivalences in the category of groups. *)
Instance hasequivs_group
  : HasEquivs Group.HasEquivs Group
Proof.HasEquivs Group
  unshelve econstructor.Group -> Group -> Type
forall a b : Group, (a $-> b) -> Type
forall a b : Group, ?CatEquiv' a b -> a $-> b
forall (a b : Group) (f : a $-> b),
?CatIsEquiv' a b f -> ?CatEquiv' a b
forall a b : Group, ?CatEquiv' a b -> b $-> a
forall (a b : Group) (f : ?CatEquiv' a b),
?CatIsEquiv' a b (?cate_fun' a b f)
forall (a b : Group) (f : a $-> b)
(fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
forall (a b : Group) (f : ?CatEquiv' a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
forall (a b : Group) (f : ?CatEquiv' a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
forall (a b : Group) (f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' a b f
  +Group -> Group -> Type exact GroupIsomorphism.
  +forall a b : Group, (a $-> b) -> Type exact (fun G H f => IsEquiv f).
  +forall a b : Group, GroupIsomorphism a b -> a $-> b intros G H f; exact f.
  +forall (a b : Group) (f : a $-> b),
(fun (G H : Group) (f0 : G $-> H) => IsEquiv f0) a b f ->
GroupIsomorphism a b exact Build_GroupIsomorphism.
  +forall a b : Group, GroupIsomorphism a b -> b $-> a intros G H; exact grp_iso_inverse.
  +forall (a b : Group) (f : GroupIsomorphism a b),
(fun (G H : Group) (f0 : G $-> H) => IsEquiv f0) a b
  ((fun (G H : Group) (f0 : GroupIsomorphism G H) =>
    isHom_GroupIsomorphism G H f0) a b f) cbn; exact _.
  +forall (a b : Group) (f : a $-> b)
(fe : (fun (G H : Group) (f0 : G $-> H) => IsEquiv f0)
        a b f),
(fun (G H : Group) (f0 : GroupIsomorphism G H) =>
 isHom_GroupIsomorphism G H f0) a b
  {| grp_iso_homo := f; isequiv_group_iso := fe |} $==
f reflexivity.
  +forall (a b : Group) (f : GroupIsomorphism a b),
(fun (G H : Group) (x : GroupIsomorphism G H) =>
 isHom_GroupIsomorphism H G (grp_iso_inverse x)) a b f $o
(fun (G H : Group) (f0 : GroupIsomorphism G H) =>
 isHom_GroupIsomorphism G H f0) a b f $== Id a intros ????; apply eissect.
  +forall (a b : Group) (f : GroupIsomorphism a b),
(fun (G H : Group) (f0 : GroupIsomorphism G H) =>
 isHom_GroupIsomorphism G H f0) a b f $o
(fun (G H : Group) (x : GroupIsomorphism G H) =>
 isHom_GroupIsomorphism H G (grp_iso_inverse x)) a b f $==
Id b intros ????; apply eisretr.
  +forall (a b : Group) (f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a ->
(fun (G H : Group) (f0 : G $-> H) => IsEquiv f0) a b f intros G H f g p q.G, H: Group
f: G $-> H
g: H $-> G
p: f $o g $== Id H
q: g $o f $== Id G
(fun (G H : Group) (f : G $-> H) => IsEquiv f) G H f
    exact (isequiv_adjointify f g p q).
Defined.

Instance is1cat_strong `{Funext} : Is1Cat_Strong Group.H: Funext
Is1Cat_Strong Group
Proof.H: Funext
Is1Cat_Strong Group
  rapply Build_Is1Cat_Strong.H: Funext
forall (a b c d : Group) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f = h $o (g $o f)
H: Funext
forall (a b c d : Group) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o (g $o f) = h $o g $o f
H: Funext
forall (a b : Group) (f : a $-> b), Id b $o f = f
H: Funext
forall (a b : Group) (f : a $-> b), f $o Id a = f
  all: intros; apply equiv_path_grouphomomorphism; intro; reflexivity.
Defined.

(** The [group_type] map is a 1-functor. *)

Instance is0functor_type_group : Is0Functor group_type.Is0Functor group_type
Proof.Is0Functor group_type
  apply Build_Is0Functor.forall a b : Group, (a $-> b) -> a $-> b
  exact @grp_homo_map.
Defined.

Instance is1functor_type_group : Is1Functor group_type.Is1Functor group_type
Proof.Is1Functor group_type
  by apply Build_Is1Functor.
Defined.

(** The [ptype_group] map is a 1-functor. *)

Instance is0functor_ptype_group : Is0Functor ptype_group.Is0Functor ptype_group
Proof.Is0Functor ptype_group
  apply Build_Is0Functor.forall a b : Group, (a $-> b) -> a $-> b
  rapply @pmap_GroupHomomorphism.
Defined.

Instance is1functor_ptype_group : Is1Functor ptype_group.Is1Functor ptype_group
Proof.Is1Functor ptype_group
  apply Build_Is1Functor; intros; by apply phomotopy_homotopy_hset.
Defined.

(** Given a group element [a0 : A] over [b : B], multiplication by [a] establishes an equivalence between the kernel and the fiber over [b]. *)
Lemma equiv_grp_hfiber {A B : Group} (f : GroupHomomorphism A B) (b : B)
  : forall (a0 : hfiber f b), hfiber f b <~> hfiber f mon_unit.A, B: Group
f: GroupHomomorphism A B
b: B
hfiber f b -> hfiber f b <~> hfiber f 1
Proof.A, B: Group
f: GroupHomomorphism A B
b: B
hfiber f b -> hfiber f b <~> hfiber f 1
  intros [a0 p].A, B: Group
f: GroupHomomorphism A B
b: B
a0: A
p: f a0 = b
hfiber f b <~> hfiber f 1
  refine (equiv_transport (hfiber f) (right_inverse b) oE _).A, B: Group
f: GroupHomomorphism A B
b: B
a0: A
p: f a0 = b
hfiber f b <~> hfiber f (b * b^)
  snapply Build_Equiv.A, B: Group
f: GroupHomomorphism A B
b: B
a0: A
p: f a0 = b
hfiber f b -> hfiber f (b * b^)
A, B: Group
f: GroupHomomorphism A B
b: B
a0: A
p: f a0 = b
IsEquiv ?equiv_fun
  {A, B: Group
f: GroupHomomorphism A B
b: B
a0: A
p: f a0 = b
hfiber f b -> hfiber f (b * b^) srapply (functor_hfiber (h := (.* a0^)) (k := (.* b^))).A, B: Group
f: GroupHomomorphism A B
b: B
a0: A
p: f a0 = b
(fun y : B => y * b^) o f ==
f o (fun y : A => y * a0^)
    intro a; cbn; symmetry.A, B: Group
f: GroupHomomorphism A B
b: B
a0: A
p: f a0 = b
a: A
f (a * a0^) = f a * b^
    rhs_V exact (ap (fun x => f a * x^) p).A, B: Group
f: GroupHomomorphism A B
b: B
a0: A
p: f a0 = b
a: A
f (a * a0^) = f a * (f a0)^
    exact (grp_homo_op f _ _ @ ap (f a *.) (grp_homo_inv f a0)). }A, B: Group
f: GroupHomomorphism A B
b: B
a0: A
p: f a0 = b
IsEquiv
  (functor_hfiber
     ((fun a : A =>
       ((grp_homo_op f a (inv a0) @
         ap (sg_op (f a)) (grp_homo_inv f a0)) @
        ap (fun x : B => f a * inv x) p)^%path
       :
       f a * b^ = f (a * a0^))
      :
      (fun y : B => y * b^) o f ==
      f o (fun y : A => y * a0^)) b)
  srapply isequiv_functor_hfiber.
Defined.

(** ** The trivial group *)

Definition grp_trivial : Group.Group
Proof.Group
  snapply (Build_Group' Unit (fun _ _ => tt) tt (fun _ => tt));
    only 1: exact _; by intros [].
Defined.

(** Map out of trivial group. *)
Definition grp_trivial_rec (G : Group) : GroupHomomorphism grp_trivial G.G: Group
GroupHomomorphism grp_trivial G
Proof.G: Group
GroupHomomorphism grp_trivial G
  snapply Build_GroupHomomorphism.G: Group
grp_trivial -> G
G: Group
IsSemiGroupPreserving ?grp_homo_map
  1: exact (fun _ => group_unit).G: Group
IsSemiGroupPreserving
  (fun _ : grp_trivial => group_unit)
  intros ??; symmetry; apply grp_unit_l.
Defined.

(** Map into trivial group. *)
Definition grp_trivial_corec (G : Group) : GroupHomomorphism G grp_trivial.G: Group
GroupHomomorphism G grp_trivial
Proof.G: Group
GroupHomomorphism G grp_trivial
  snapply Build_GroupHomomorphism.G: Group
G -> grp_trivial
G: Group
IsSemiGroupPreserving ?grp_homo_map
  1: exact (fun _ => tt).G: Group
IsSemiGroupPreserving (fun _ : G => tt)
  intros ??; symmetry; exact (grp_unit_l _).
Defined.

(** Group is a pointed category. *)
Instance ispointedcat_group : IsPointedCat Group.IsPointedCat Group
Proof.IsPointedCat Group
  snapply Build_IsPointedCat.Group
IsInitial ?zero_object
IsTerminal ?zero_object
  -Group exact grp_trivial.
  -IsInitial grp_trivial intro G.G: Group
{f : grp_trivial $-> G &
forall g : grp_trivial $-> G, f $== g}
    exists (grp_trivial_rec G).G: Group
forall g : grp_trivial $-> G, grp_trivial_rec G $== g
    intros g []; cbn.G: Group
g: grp_trivial $-> G
group_unit = g tt
    exact (grp_homo_unit g)^%path.
  -IsTerminal grp_trivial intro G.G: Group
{f : G $-> grp_trivial &
forall g : G $-> grp_trivial, f $== g}
    exists (grp_trivial_corec G).G: Group
forall g : G $-> grp_trivial,
grp_trivial_corec G $== g
    intros g x; cbn.G: Group
g: G $-> grp_trivial
x: G
tt = g x
    apply path_unit.
Defined.

Definition grp_homo_const {G H : Group} : GroupHomomorphism G H
  := zero_morphism.

(** ** Opposite Group *)

(** The opposite group of a group is the group with the same elements but with the group operation reversed. Our technical choice for including a redundant associativity axiom in the definition of a group from before comes into play here. All we have to do to define the opposite group is to shuffle some data around. Since we are only shuffling, this operation becomes definitionally involutive. We make this choice because it is a great help in later proofs.  *)
Definition grp_op : Group -> Group.Group -> Group
Proof.Group -> Group
  intros G.G: Group
Group
  snapply Build_Group_internal; repeat split.G: Group
Type
G: Group
SgOp ?group_type
G: Group
MonUnit ?group_type
G: Group
Inverse ?group_type
G: Group
IsHSet ?group_type
G: Group
Associative sg_op
G: Group
LeftIdentity sg_op 1
G: Group
RightIdentity sg_op 1
G: Group
LeftInverse sg_op inv 1
G: Group
RightInverse sg_op inv 1
G: Group
Associative (flip ?group_sgop)
  -G: Group
Type exact G.
  -G: Group
SgOp G exact (flip (.*.)).
  -G: Group
MonUnit G exact 1.
  -G: Group
Inverse G exact (^).
  -G: Group
IsHSet G exact _.
  -G: Group
Associative sg_op exact group_assoc_opp.
  -G: Group
LeftIdentity sg_op 1 exact grp_unit_r.
  -G: Group
RightIdentity sg_op 1 exact grp_unit_l.
  -G: Group
LeftInverse sg_op inv 1 exact grp_inv_r.
  -G: Group
RightInverse sg_op inv 1 exact grp_inv_l.
  -G: Group
Associative (flip (flip sg_op)) exact grp_assoc.
Defined.

(** Taking the inverse is an isomorphism from the group to the opposite group. *)
Definition grp_op_iso_inv (G : Group)
  : G $<~> (grp_op G).G: Group
G ≅ grp_op G
Proof.G: Group
G ≅ grp_op G
  snapply Build_GroupIsomorphism.G: Group
GroupHomomorphism G (grp_op G)
G: Group
IsEquiv ?grp_iso_homo
  -G: Group
GroupHomomorphism G (grp_op G) snapply Build_GroupHomomorphism.G: Group
G -> grp_op G
G: Group
IsSemiGroupPreserving ?grp_homo_map
    +G: Group
G -> grp_op G exact inv.
    +G: Group
IsSemiGroupPreserving inv intros x y.G: Group
x, y: G
(x * y)^ = x^ * y^
      rapply grp_inv_op.
  -G: Group
IsEquiv
  {|
    grp_homo_map := inv;
    issemigrouppreserving_grp_homo :=
      (fun x y : G => grp_inv_op y x)
      :
      IsSemiGroupPreserving inv
  |} simpl; exact _.
Defined.

(** ** The direct product of groups *)

(** The cartesian product of the underlying sets of two groups has a natural group structure. We call this the direct product of groups. *)
Definition grp_prod : Group -> Group -> Group.Group -> Group -> Group
Proof.Group -> Group -> Group
  intros G H.G, H: Group
Group
  snapply (Build_Group (G * H)).G, H: Group
SgOp (G * H)
G, H: Group
MonUnit (G * H)
G, H: Group
Inverse (G * H)
G, H: Group
IsGroup (G * H)
  4: repeat split.G, H: Group
SgOp (G * H)
G, H: Group
MonUnit (G * H)
G, H: Group
Inverse (G * H)
G, H: Group
IsHSet (G * H)
G, H: Group
Associative sg_op
G, H: Group
LeftIdentity sg_op 1
G, H: Group
RightIdentity sg_op 1
G, H: Group
LeftInverse sg_op inv 1
G, H: Group
RightInverse sg_op inv 1
  -G, H: Group
SgOp (G * H) intros [g1 h1] [g2 h2].G, H: Group
g1: G
h1: H
g2: G
h2: H
(G * H)%type
    exact (g1 * g2, h1 * h2).
  -G, H: Group
MonUnit (G * H) exact (1, 1).
  -G, H: Group
Inverse (G * H) exact (functor_prod inv inv).
  -G, H: Group
IsHSet (G * H) exact _.
  -G, H: Group
Associative sg_op intros x y z; apply path_prod'; apply simple_associativity.
  -G, H: Group
LeftIdentity sg_op 1 intros x; apply path_prod'; apply left_identity.
  -G, H: Group
RightIdentity sg_op 1 intros x; apply path_prod'; apply right_identity.
  -G, H: Group
LeftInverse sg_op inv 1 intros x; apply path_prod'; apply left_inverse.
  -G, H: Group
RightInverse sg_op inv 1 intros x; apply path_prod'; apply right_inverse.
Defined.

(** Maps into the direct product can be built by mapping separately into each factor. *)
Proposition grp_prod_corec {G H K : Group} (f : K $-> G) (g : K $-> H)
  : K $-> (grp_prod G H).G, H, K: Group
f: K $-> G
g: K $-> H
K $-> grp_prod G H
Proof.G, H, K: Group
f: K $-> G
g: K $-> H
K $-> grp_prod G H
  snapply Build_GroupHomomorphism.G, H, K: Group
f: K $-> G
g: K $-> H
K -> grp_prod G H
G, H, K: Group
f: K $-> G
g: K $-> H
IsSemiGroupPreserving ?grp_homo_map
  -G, H, K: Group
f: K $-> G
g: K $-> H
K -> grp_prod G H exact (fun x : K => (f x, g x)).
  -G, H, K: Group
f: K $-> G
g: K $-> H
IsSemiGroupPreserving (fun x : K => (f x, g x)) intros x y.G, H, K: Group
f: K $-> G
g: K $-> H
x, y: K
(f (x * y), g (x * y)) = (f x, g x) * (f y, g y)
    apply path_prod'; apply grp_homo_op.
Defined.

(** [grp_prod_corec] satisfies a definitional naturality property. *)
Definition grp_prod_corec_natural {X Y A B : Group}
  (f : X $-> Y) (g0 : Y $-> A) (g1 : Y $-> B)
  : grp_prod_corec g0 g1 $o f $== grp_prod_corec (g0 $o f) (g1 $o f)
  := fun _ => idpath.

(** The left factor injects into the direct product. *)
Definition grp_prod_inl {H K : Group}
  : H $-> grp_prod H K
  := grp_prod_corec grp_homo_id grp_homo_const.

(** The left injection is an embedding. *)
Instance isembedding_grp_prod_inl {H K : Group}
  : IsEmbedding (@grp_prod_inl H K).H, K: Group
IsEmbedding grp_prod_inl
Proof.H, K: Group
IsEmbedding grp_prod_inl
  apply isembedding_isinj_hset.H, K: Group
IsInjective grp_prod_inl
  intros h0 h1 p; cbn in p.H, K: Group
h0, h1: H
p: (h0, group_unit) = (h1, group_unit)
h0 = h1
  exact (fst ((equiv_path_prod _ _)^-1 p)).
Defined.

(** The right factor injects into the direct product. *)
Definition grp_prod_inr {H K : Group}
  : K $-> grp_prod H K
  := grp_prod_corec grp_homo_const grp_homo_id.

(** The right injection is an embedding. *)
Instance isembedding_grp_prod_inr {H K : Group}
  : IsEmbedding (@grp_prod_inr H K).H, K: Group
IsEmbedding grp_prod_inr
Proof.H, K: Group
IsEmbedding grp_prod_inr
  apply isembedding_isinj_hset.H, K: Group
IsInjective grp_prod_inr
  intros k0 k1 q; cbn in q.H, K: Group
k0, k1: K
q: (group_unit, k0) = (group_unit, k1)
k0 = k1
  exact (snd ((equiv_path_prod _ _)^-1 q)).
Defined.

(** Given two pairs of isomorphic groups, their pairwise direct products are isomorphic. *)
Definition grp_iso_prod {A B C D : Group}
  : A ≅ B -> C ≅ D -> (grp_prod A C) ≅ (grp_prod B D).A, B, C, D: Group
A ≅ B -> C ≅ D -> grp_prod A C ≅ grp_prod B D
Proof.A, B, C, D: Group
A ≅ B -> C ≅ D -> grp_prod A C ≅ grp_prod B D
  intros f g.A, B, C, D: Group
f: A ≅ B
g: C ≅ D
grp_prod A C ≅ grp_prod B D
  srapply Build_GroupIsomorphism'.A, B, C, D: Group
f: A ≅ B
g: C ≅ D
grp_prod A C <~> grp_prod B D
A, B, C, D: Group
f: A ≅ B
g: C ≅ D
IsSemiGroupPreserving ?f
  1: exact (equiv_functor_prod (f:=f) (g:=g)).A, B, C, D: Group
f: A ≅ B
g: C ≅ D
IsSemiGroupPreserving equiv_functor_prod
  simpl.A, B, C, D: Group
f: A ≅ B
g: C ≅ D
IsSemiGroupPreserving (functor_prod f g)
  unfold functor_prod.A, B, C, D: Group
f: A ≅ B
g: C ≅ D
IsSemiGroupPreserving
  (fun z : A * C => (f (fst z), g (snd z)))
  intros x y.A, B, C, D: Group
f: A ≅ B
g: C ≅ D
x, y: (A * C)%type
(f (fst (x * y)), g (snd (x * y))) =
(f (fst x), g (snd x)) * (f (fst y), g (snd y))
  apply path_prod.A, B, C, D: Group
f: A ≅ B
g: C ≅ D
x, y: (A * C)%type
fst (f (fst (x * y)), g (snd (x * y))) =
fst ((f (fst x), g (snd x)) * (f (fst y), g (snd y)))
A, B, C, D: Group
f: A ≅ B
g: C ≅ D
x, y: (A * C)%type
snd (f (fst (x * y)), g (snd (x * y))) =
snd ((f (fst x), g (snd x)) * (f (fst y), g (snd y)))
  1,2: apply grp_homo_op.
Defined.

(** The first projection of the direct product. *)
Definition grp_prod_pr1 {G H : Group}
  : GroupHomomorphism (grp_prod G H) G.G, H: Group
GroupHomomorphism (grp_prod G H) G
Proof.G, H: Group
GroupHomomorphism (grp_prod G H) G
  snapply Build_GroupHomomorphism.G, H: Group
grp_prod G H -> G
G, H: Group
IsSemiGroupPreserving ?grp_homo_map
  1: exact fst.G, H: Group
IsSemiGroupPreserving fst
  intros ? ?; reflexivity.
Defined.

(** The first projection is a surjection. *)
Instance issurj_grp_prod_pr1 {G H : Group}
  : IsSurjection (@grp_prod_pr1 G H)
  := issurj_retr grp_prod_inl (fun _ => idpath).

(** The second projection of the direct product. *)
Definition grp_prod_pr2 {G H : Group}
  : GroupHomomorphism (grp_prod G H) H.G, H: Group
GroupHomomorphism (grp_prod G H) H
Proof.G, H: Group
GroupHomomorphism (grp_prod G H) H
  snapply Build_GroupHomomorphism.G, H: Group
grp_prod G H -> H
G, H: Group
IsSemiGroupPreserving ?grp_homo_map
  1: exact snd.G, H: Group
IsSemiGroupPreserving snd
  intros ? ?; reflexivity.
Defined.

(** Pairs in direct products can be decomposed *)
Definition grp_prod_decompose {G H : Group} (g : G) (h : H)
  : (g, h) = ((g, 1) : grp_prod G H) * (1, h).G, H: Group
g: G
h: H
(g, h) = ((g, 1) : grp_prod G H) * (1, h)
Proof.G, H: Group
g: G
h: H
(g, h) = ((g, 1) : grp_prod G H) * (1, h)
  snapply path_prod; symmetry.G, H: Group
g: G
h: H
fst (((g, 1) : grp_prod G H) * (1, h)) = fst (g, h)
G, H: Group
g: G
h: H
snd (((g, 1) : grp_prod G H) * (1, h)) = snd (g, h)
  -G, H: Group
g: G
h: H
fst (((g, 1) : grp_prod G H) * (1, h)) = fst (g, h) snapply grp_unit_r.
  -G, H: Group
g: G
h: H
snd (((g, 1) : grp_prod G H) * (1, h)) = snd (g, h) snapply grp_unit_l.
Defined.

(** The second projection is a surjection. *)
Instance issurj_grp_prod_pr2 {G H : Group}
  : IsSurjection (@grp_prod_pr2 G H)
  := issurj_retr grp_prod_inr (fun _ => idpath).

(** [Group] is a category with binary products given by the direct product. *)
Instance hasbinaryproducts_group : HasBinaryProducts Group.HasBinaryProducts Group
Proof.HasBinaryProducts Group
  intros G H.G, H: Group
BinaryProduct G H
  snapply Build_BinaryProduct.G, H: Group
Group
G, H: Group
?cat_binprod' $-> G
G, H: Group
?cat_binprod' $-> H
G, H: Group
forall z : Group,
(z $-> G) -> (z $-> H) -> z $-> ?cat_binprod'
G, H: Group
forall (z : Group) (f : z $-> G) (g : z $-> H),
?cat_pr1 $o ?cat_binprod_corec z f g $== f
G, H: Group
forall (z : Group) (f : z $-> G) (g : z $-> H),
?cat_pr2 $o ?cat_binprod_corec z f g $== g
G, H: Group
forall (z : Group) (f g : z $-> ?cat_binprod'),
?cat_pr1 $o f $== ?cat_pr1 $o g ->
?cat_pr2 $o f $== ?cat_pr2 $o g -> f $== g
  -G, H: Group
Group exact (grp_prod G H).
  -G, H: Group
grp_prod G H $-> G exact grp_prod_pr1.
  -G, H: Group
grp_prod G H $-> H exact grp_prod_pr2.
  -G, H: Group
forall z : Group,
(z $-> G) -> (z $-> H) -> z $-> grp_prod G H intros K.G, H, K: Group
(K $-> G) -> (K $-> H) -> K $-> grp_prod G H
    exact grp_prod_corec.
  -G, H: Group
forall (z : Group) (f : z $-> G) (g : z $-> H),
grp_prod_pr1 $o
(fun K : Group => grp_prod_corec) z f g $== f intros K f g.G, H, K: Group
f: K $-> G
g: K $-> H
grp_prod_pr1 $o
(fun K : Group => grp_prod_corec) K f g $== f
    exact (Id _).
  -G, H: Group
forall (z : Group) (f : z $-> G) (g : z $-> H),
grp_prod_pr2 $o
(fun K : Group => grp_prod_corec) z f g $== g intros K f g.G, H, K: Group
f: K $-> G
g: K $-> H
grp_prod_pr2 $o
(fun K : Group => grp_prod_corec) K f g $== g
    exact (Id _).
  -G, H: Group
forall (z : Group) (f g : z $-> grp_prod G H),
grp_prod_pr1 $o f $== grp_prod_pr1 $o g ->
grp_prod_pr2 $o f $== grp_prod_pr2 $o g -> f $== g intros K f g p q a.G, H, K: Group
f, g: K $-> grp_prod G H
p: grp_prod_pr1 $o f $== grp_prod_pr1 $o g
q: grp_prod_pr2 $o f $== grp_prod_pr2 $o g
a: K
f a = g a
    exact (path_prod' (p a) (q a)).
Defined.

(** *** Properties of maps to and from the trivial group *)

Instance isinitial_grp_trivial : IsInitial grp_trivial.IsInitial grp_trivial
Proof.IsInitial grp_trivial
  intro G.G: Group
{f : grp_trivial $-> G &
forall g : grp_trivial $-> G, f $== g}
  exists (grp_trivial_rec _).G: Group
forall g : grp_trivial $-> G, grp_trivial_rec G $== g
  intros g [].G: Group
g: grp_trivial $-> G
grp_trivial_rec G tt = g tt
  exact (grp_homo_unit g)^%path.
Defined.

Instance contr_grp_homo_trivial_source `{Funext} G
  : Contr (GroupHomomorphism grp_trivial G).H: Funext
G: Group
Contr (GroupHomomorphism grp_trivial G)
Proof.H: Funext
G: Group
Contr (GroupHomomorphism grp_trivial G)
  snapply Build_Contr.H: Funext
G: Group
GroupHomomorphism grp_trivial G
H: Funext
G: Group
forall y : GroupHomomorphism grp_trivial G,
?center = y
  1: exact (grp_trivial_rec _).H: Funext
G: Group
forall y : GroupHomomorphism grp_trivial G,
grp_trivial_rec G = y
  intros g.H: Funext
G: Group
g: GroupHomomorphism grp_trivial G
grp_trivial_rec G = g
  rapply equiv_path_grouphomomorphism.H: Funext
G: Group
g: GroupHomomorphism grp_trivial G
grp_trivial_rec G == g
  intros [].H: Funext
G: Group
g: GroupHomomorphism grp_trivial G
grp_trivial_rec G tt = g tt
  symmetry.H: Funext
G: Group
g: GroupHomomorphism grp_trivial G
g tt = grp_trivial_rec G tt
  rapply grp_homo_unit.
Defined.

Instance isterminal_grp_trivial : IsTerminal grp_trivial.IsTerminal grp_trivial
Proof.IsTerminal grp_trivial
  intro G.G: Group
{f : G $-> grp_trivial &
forall g : G $-> grp_trivial, f $== g}
  exists (grp_trivial_corec _).G: Group
forall g : G $-> grp_trivial,
grp_trivial_corec G $== g
  intros g x.G: Group
g: G $-> grp_trivial
x: G
grp_trivial_corec G x = g x
  apply path_contr.
Defined.

Instance contr_grp_homo_trivial_target `{Funext} G
  : Contr (GroupHomomorphism G grp_trivial).H: Funext
G: Group
Contr (GroupHomomorphism G grp_trivial)
Proof.H: Funext
G: Group
Contr (GroupHomomorphism G grp_trivial)
  snapply Build_Contr.H: Funext
G: Group
GroupHomomorphism G grp_trivial
H: Funext
G: Group
forall y : GroupHomomorphism G grp_trivial,
?center = y
  1: exact (pr1 (isterminal_grp_trivial _)).H: Funext
G: Group
forall y : GroupHomomorphism G grp_trivial,
(isterminal_grp_trivial G).1 = y
  intros g.H: Funext
G: Group
g: GroupHomomorphism G grp_trivial
(isterminal_grp_trivial G).1 = g
  rapply equiv_path_grouphomomorphism.H: Funext
G: Group
g: GroupHomomorphism G grp_trivial
(isterminal_grp_trivial G).1 == g
  intros x.H: Funext
G: Group
g: GroupHomomorphism G grp_trivial
x: G
(isterminal_grp_trivial G).1 x = g x
  apply path_contr.
Defined.

Instance ishprop_grp_iso_trivial `{Funext} (G : Group)
  : IsHProp (G ≅ grp_trivial).H: Funext
G: Group
IsHProp (G ≅ grp_trivial)
Proof.H: Funext
G: Group
IsHProp (G ≅ grp_trivial)
  apply equiv_hprop_allpath.H: Funext
G: Group
forall x y : G ≅ grp_trivial, x = y
  intros f g.H: Funext
G: Group
f, g: G ≅ grp_trivial
f = g
  apply equiv_path_groupisomorphism; intro; apply path_ishprop.
Defined.

(** ** Free groups *)

Definition FactorsThroughFreeGroup (S : Type) (F_S : Group)
  (i : S -> F_S) (A : Group) (g : S -> A) : Type
  := {f : F_S $-> A & f o i == g}.

(** Universal property of a free group on a set (type). *)
Class IsFreeGroupOn (S : Type) (F_S : Group) (i : S -> F_S)
  := contr_isfreegroupon :: forall (A : Group) (g : S -> A),
      Contr (FactorsThroughFreeGroup S F_S i A g).

(** A group is free if there exists a generating type on which it is a free group. *)
Class IsFreeGroup (F_S : Group)
  := isfreegroup : {S : _ & {i : _ & IsFreeGroupOn S F_S i}}.

Instance isfreegroup_isfreegroupon (S : Type) (F_S : Group) (i : S -> F_S)
  {H : IsFreeGroupOn S F_S i}
  : IsFreeGroup F_S
  := (S; i; H).


(** ** Further properties of group homomorphisms. *)

(** Commutativity can be transferred across isomorphisms. *)
Definition commutative_iso_commutative {G H : Group}
  {C : Commutative (@group_sgop G)} (f : GroupIsomorphism G H)
  : Commutative (@group_sgop H).G, H: Group
C: Commutative group_sgop
f: GroupIsomorphism G H
Commutative group_sgop
Proof.G, H: Group
C: Commutative group_sgop
f: GroupIsomorphism G H
Commutative group_sgop
  unfold Commutative.G, H: Group
C: Commutative group_sgop
f: GroupIsomorphism G H
forall x y : H, group_sgop x y = group_sgop y x
  rapply (equiv_ind f); intro g1.G, H: Group
C: Commutative group_sgop
f: GroupIsomorphism G H
g1: G
forall y : H,
group_sgop (f g1) y = group_sgop y (f g1)
  rapply (equiv_ind f); intro g2.G, H: Group
C: Commutative group_sgop
f: GroupIsomorphism G H
g1, g2: G
group_sgop (f g1) (f g2) = group_sgop (f g2) (f g1)
  refine ((preserves_sg_op _ _)^ @ _ @ (preserves_sg_op _ _)).G, H: Group
C: Commutative group_sgop
f: GroupIsomorphism G H
g1, g2: G
f (g1 * g2) = f (g2 * g1)
  refine (ap f _).G, H: Group
C: Commutative group_sgop
f: GroupIsomorphism G H
g1, g2: G
g1 * g2 = g2 * g1
  apply C.
Defined.

(** If two group homomorphisms agree on two elements, then they agree on their product. *)
Definition grp_homo_op_agree {G G' H : Group} (f : G $-> H) (f' : G' $-> H)
  {x y : G} {x' y' : G'} (p : f x = f' x') (q : f y = f' y')
  : f (x * y) = f' (x' * y').G, G', H: Group
f: G $-> H
f': G' $-> H
x, y: G
x', y': G'
p: f x = f' x'
q: f y = f' y'
f (x * y) = f' (x' * y')
Proof.G, G', H: Group
f: G $-> H
f': G' $-> H
x, y: G
x', y': G'
p: f x = f' x'
q: f y = f' y'
f (x * y) = f' (x' * y')
  lhs napply grp_homo_op.G, G', H: Group
f: G $-> H
f': G' $-> H
x, y: G
x', y': G'
p: f x = f' x'
q: f y = f' y'
f x * f y = f' (x' * y')
  rhs napply grp_homo_op.G, G', H: Group
f: G $-> H
f': G' $-> H
x, y: G
x', y': G'
p: f x = f' x'
q: f y = f' y'
f x * f y = f' x' * f' y'
  exact (ap011 _ p q).
Defined.

(** The group movement lemmas can be extended to when there is a homomorphism involved.  For now, we only include these two. *)
Definition grp_homo_moveL_1V {A B : Group} (f : GroupHomomorphism A B) (x y : A)
  : f (x * y) = group_unit <~> (f x = - f y)
  := grp_moveL_1V oE equiv_concat_l (grp_homo_op f x y)^ _.

Definition grp_homo_moveL_1M  {A B : Group} (f : GroupHomomorphism A B) (x y : A)
  : f (x * y^) = group_unit <~> (f x = f y).A, B: Group
f: GroupHomomorphism A B
x, y: A
f (x * y^) = group_unit <~> f x = f y
Proof.A, B: Group
f: GroupHomomorphism A B
x, y: A
f (x * y^) = group_unit <~> f x = f y
  refine (grp_moveL_1M oE equiv_concat_l _^ _).A, B: Group
f: GroupHomomorphism A B
x, y: A
f (x * y^) = f x * (f y)^
  lhs napply grp_homo_op.A, B: Group
f: GroupHomomorphism A B
x, y: A
f x * f y^ = f x * (f y)^
  apply ap, grp_homo_inv.
Defined.

(** ** Conjugation *)

(** Conjugation by a group element is a homomorphism. Often we need to use properties about group homomorphisms in order to prove things about conjugation, so it is helpful to define it directly as a group homomorphism. *)
Definition grp_conj {G : Group} (x : G) : G $-> G.G: Group
x: G
G $-> G
Proof.G: Group
x: G
G $-> G
  snapply Build_GroupHomomorphism.G: Group
x: G
G -> G
G: Group
x: G
IsSemiGroupPreserving ?grp_homo_map
  -G: Group
x: G
G -> G exact (fun y => x * y * x^).
  -G: Group
x: G
IsSemiGroupPreserving (fun y : G => x * y * x^) intros y z.G: Group
x, y, z: G
x * (y * z) * x^ = x * y * x^ * (x * z * x^)
    rhs napply grp_assoc.G: Group
x, y, z: G
x * (y * z) * x^ = x * y * x^ * (x * z) * x^
    apply (ap (.* x^)).G: Group
x, y, z: G
x * (y * z) = x * y * x^ * (x * z)
    rhs napply grp_assoc.G: Group
x, y, z: G
x * (y * z) = x * y * x^ * x * z
    lhs napply grp_assoc.G: Group
x, y, z: G
x * y * z = x * y * x^ * x * z
    apply (ap (.* z)).G: Group
x, y, z: G
x * y = x * y * x^ * x
    symmetry; apply grp_inv_gV_g.
Defined.

(** Conjugation by the unit element is the identity. *)
Definition grp_conj_unit {G : Group} : grp_conj (G:=G) 1 $== Id _.G: Group
grp_conj 1 $== Id G
Proof.G: Group
grp_conj 1 $== Id G
  intros x.G: Group
x: G
grp_conj 1 x = Id G x
  apply grp_moveR_gV.G: Group
x: G
1 * x = Id G x * 1
  by napply grp_1g_g1.
Defined.

(** Conjugation commutes with group homomorphisms. *)
Definition grp_homo_conj {G H : Group} (f : G $-> H) (x : G)
  : f $o grp_conj x $== grp_conj (f x) $o f.G, H: Group
f: G $-> H
x: G
f $o grp_conj x $== grp_conj (f x) $o f
Proof.G, H: Group
f: G $-> H
x: G
f $o grp_conj x $== grp_conj (f x) $o f
  intros z; simpl.G, H: Group
f: G $-> H
x, z: G
f (x * z * x^) = f x * f z * (f x)^
  by rewrite !grp_homo_op, grp_homo_inv.
Defined.

(** Conjugation respects composition. *)
Definition grp_conj_op {G : Group} (x y : G)
  : grp_conj (x * y) $== grp_conj x $o grp_conj y.G: Group
x, y: G
grp_conj (x * y) $== grp_conj x $o grp_conj y
Proof.G: Group
x, y: G
grp_conj (x * y) $== grp_conj x $o grp_conj y
  intros z; simpl.G: Group
x, y, z: G
x * y * z * (x * y)^ = x * (y * z * y^) * x^
  by rewrite grp_inv_op, !grp_assoc.
Defined.

(** Conjugating by an element then its inverse is the identity. *)
Definition grp_conj_inv_r {G : Group} (x : G)
  : grp_conj x $o grp_conj x^ $== Id _.G: Group
x: G
grp_conj x $o grp_conj x^ $== Id G
Proof.G: Group
x: G
grp_conj x $o grp_conj x^ $== Id G
  refine ((grp_conj_op _ _)^$ $@ _ $@ grp_conj_unit).G: Group
x: G
grp_conj (x * x^) $== grp_conj 1
  intros y.G: Group
x, y: G
grp_conj (x * x^) y = grp_conj 1 y
  napply (ap (fun x => grp_conj x y)).G: Group
x, y: G
x * x^ = 1
  apply grp_inv_r.
Defined.

(** Conjugating by an inverse then the element is the identity. *)
Definition grp_conj_inv_l {G : Group} (x : G)
  : grp_conj x^ $o grp_conj x $== Id _.G: Group
x: G
grp_conj x^ $o grp_conj x $== Id G
Proof.G: Group
x: G
grp_conj x^ $o grp_conj x $== Id G
  refine ((grp_conj_op _ _)^$ $@ _ $@ grp_conj_unit).G: Group
x: G
grp_conj (x^ * x) $== grp_conj 1
  intros y.G: Group
x, y: G
grp_conj (x^ * x) y = grp_conj 1 y
  napply (ap (fun x => grp_conj x y)).G: Group
x, y: G
x^ * x = 1
  apply grp_inv_l.
Defined.

(** Conjugation is a group automorphism. *)
Definition grp_iso_conj {G : Group} (x : G) : G $<~> G
  := cate_adjointify (grp_conj x) (grp_conj x^)
      (grp_conj_inv_r _) (grp_conj_inv_l _).