Merge pull request #2200 from Alizter/style-tweaks-groups

minor cleanups in Groups/
HoTT · Jan 19, 2025 · 1498a67 · 1498a67
2 parents 6ae0f16 + 3cdf2c6
commit 1498a67
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 6 deletions.
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
@@ -930,7 +930,7 @@ Definition grp_prod_corec_natural {X Y A B : Group}
 
 (** The left factor injects into the direct product. *)
 Definition grp_prod_inl {H K : Group}
-  : H $-> (grp_prod H K)
+  : H $-> grp_prod H K
   := grp_prod_corec grp_homo_id grp_homo_const.
 
 (** The left injection is an embedding. *)
@@ -944,7 +944,7 @@ Defined.
 
 (** The right factor injects into the direct product. *)
 Definition grp_prod_inr {H K : Group}
-  : K $-> (grp_prod H K)
+  : K $-> grp_prod H K
   := grp_prod_corec grp_homo_const grp_homo_id.
 
 (** The right injection is an embedding. *)
@@ -995,7 +995,7 @@ Defined.
 
 (** Pairs in direct products can be decomposed *)
 Definition grp_prod_decompose {G H : Group} (g : G) (h : H)
-  : (g, h) = ((g, group_unit) : grp_prod G H) * (group_unit, h).
+  : (g, h) = ((g, 1) : grp_prod G H) * (1, h).
 Proof.
   snrapply path_prod; symmetry.
   - snrapply grp_unit_r.

diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
@@ -253,9 +253,8 @@ Section FirstIso.
     snrapply isequiv_surj_emb.
     1: srapply cancelR_conn_map.
     srapply isembedding_isinj_hset.
-    refine (Quotient_ind_hprop _ _ _); intro x.
-    refine (Quotient_ind_hprop _ _ _); intro y.
-    intros h; simpl in h.
+    srapply Quotient_ind2_hprop.
+    intros x y h; simpl in h.
     apply qglue; cbn.
     apply (equiv_path_sigma_hprop _ _)^-1%equiv in h; cbn in h.
     cbn. rewrite grp_homo_op, grp_homo_inv, h.