diff --git a/Cubical.Algebra.AbGroup.Base.html b/Cubical.Algebra.AbGroup.Base.html
index 092d5e13c5..c859e5f451 100644
--- a/Cubical.Algebra.AbGroup.Base.html
+++ b/Cubical.Algebra.AbGroup.Base.html
@@ -346,9 +346,9 @@
isAbGroup (snd HomGroup) =
makeIsAbGroup
isSetGroupHom
- (λ { (f , p) (g , q) (h , r) → Σ≡Prop (λ _ → isPropIsGroupHom _ _)
+ (λ { (f , p) (g , q) (h , r) → Σ≡Prop (λ _ → isPropIsGroupHom _ _)
(funExt λ x → +AssocB _ _ _) })
- (λ { (f , p) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ y → +IdRB _)})
- ((λ { (f , p) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ y → +InvRB _)}))
- (λ { (f , p) (g , q) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ x → +CommB _ _)})
+ (λ { (f , p) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ y → +IdRB _)})
+ ((λ { (f , p) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ y → +InvRB _)}))
+ (λ { (f , p) (g , q) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ x → +CommB _ _)})