diff --git a/theories/Algebra/AbGroups/Centralizer.v b/theories/Algebra/AbGroups/Centralizer.v
index 8c3a8da8f7..6e0aceacd7 100644
--- a/theories/Algebra/AbGroups/Centralizer.v
+++ b/theories/Algebra/AbGroups/Centralizer.v
@@ -11,10 +11,8 @@ Local Open Scope mc_mult_scope.
 Definition centralizer {G : Group} (g : G)
   := fun h => g * h = h * g.
 
-Definition centralizer_unit {G : Group} (g : G) : centralizer g mon_unit.
-Proof.
-  exact (grp_unit_r _ @ (grp_unit_l _)^).
-Defined.
+Definition centralizer_unit {G : Group} (g : G) : centralizer g mon_unit
+  := grp_g1_1g _ _ idpath.
 
 Definition centralizer_sgop {G : Group} (g h k : G)
            (p : centralizer g h) (q : centralizer g k)
@@ -33,7 +31,7 @@ Definition centralizer_inverse {G : Group} (g h : G)
 Proof.
   unfold centralizer in *.
   symmetry.
-  refine ((grp_unit_r _)^ @ _ @ grp_unit_l _).
+  apply grp_g1_1g.
   refine (ap ((_ * g) *.) (grp_inv_r h)^ @ _ @ ap (.* (g * _)) (grp_inv_l h)).
   refine (grp_assoc _ _ _ @ _ @ (grp_assoc _ _ _)^).
   refine (ap (.* h^) _).
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 2c489454e5..76d1d782d8 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -465,6 +465,12 @@ Section GroupEquations.
   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.
 
 (** ** Cancelation lemmas *)
@@ -678,7 +684,7 @@ Definition grp_pow_commutes {G : Group} (n : Int) (g h : G)
   : h * (grp_pow g n) = (grp_pow g n) * h.
 Proof.
   induction n.
-  - exact (grp_unit_r _ @ (grp_unit_l _)^).
+  - by apply grp_g1_1g.
   - rewrite grp_pow_succ.
     nrapply grp_commutes_op; assumption.
   - rewrite grp_pow_pred.
@@ -1168,8 +1174,7 @@ Definition grp_conj_unit {G : Group} : grp_conj (G:=G) 1 $== Id _.
 Proof.
   intros x.
   apply grp_moveR_gV.
-  rhs nrapply grp_unit_r.
-  nrapply grp_unit_l.
+  by nrapply grp_1g_g1.
 Defined.
 
 (** Conjugation commutes with group homomorphisms. *)
diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 0f948f354b..6b3f35ea63 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -1,4 +1,4 @@
-Require Import Basics Types HFiber WildCat.Core.
+Require Import Basics Types HFiber WildCat.Core WildCat.Equiv.
 Require Import Truncations.Core.
 Require Import Algebra.Groups.Group TruncType.
 
@@ -188,6 +188,13 @@ Proof.
   apply inverse_mon_unit.
 Defined.
 
+Definition trivial_subgroup_rec {G : Group} (H : Subgroup G)
+  : forall x, trivial_subgroup G x -> H x.
+Proof.
+  snrapply paths_ind_r; cbn beta.
+  apply issubgroup_in_unit.
+Defined.
+
 (** The preimage of a subgroup under a group homomorphism is a subgroup. *)
 Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H)
   : Subgroup G.
@@ -497,14 +504,38 @@ Proof.
   exact p.
 Defined.
 
-(** The property of being the trivial subgroup is useful. *)
-Definition IsTrivialSubgroup {G : Group} (H : Subgroup G) : Type :=
-  forall x, H x <-> trivial_subgroup G x.
-Existing Class IsTrivialSubgroup.
-
-Global Instance istrivialsubgroup_trivial_subgroup {G : Group}
-  : IsTrivialSubgroup (@trivial_subgroup G)
-  := ltac:(hnf; reflexivity).
+(** The property of being the trivial group is useful. Note that any group can be automatically coerced to its maximal subgroup, so it makes sense for this predicate to be applied to groups in general. *)
+Class IsTrivialGroup@{i} {G : Group@{i}} (H : Subgroup@{i i} G) :=
+  istrivialgroup : forall x, H x -> trivial_subgroup G x.
+
+Global Instance istrivial_trivial_subgroup {G : Group}
+  : IsTrivialGroup (trivial_subgroup G)
+  := fun x => idmap.
+
+(** Trivial groups are isomorphic to the trivial group. *)
+Definition istrivial_iff_grp_iso_trivial_subgroup {G : Group} (H : Subgroup G)
+  : IsTrivialGroup H
+    <-> (subgroup_group H $<~> subgroup_group (trivial_subgroup G)).
+Proof.
+  split.
+  - intros T.
+    snrapply Build_GroupIsomorphism'.
+    + snrapply equiv_functor_sigma_id.
+      intros x.
+      rapply equiv_iff_hprop_uncurried.
+      split; only 1: apply T.
+      apply trivial_subgroup_rec.
+    + intros [x Hx] [y Hy].
+      by rapply path_sigma_hprop.
+  - unfold IsTrivialGroup.
+    intros e x h.
+    change ((x; h).1 = (1; idpath).1).
+    snrapply (pr1_path (u:=(_;_)) (v:=(_;_))).
+    1: apply subgroup_in_unit.
+    rhs_V nrapply (grp_homo_unit e^-1$).
+    apply moveL_equiv_V.
+    apply path_contr.
+Defined.
 
 (** Intersection of two subgroups *)
 Definition subgroup_intersection {G : Group} (H K : Subgroup G) : Subgroup G.