workinonit

UniMath · Feb 16, 2025 · 7dbe6de · 7dbe6de
1 parent 14a7113
commit 7dbe6de
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 4 deletions.
diff --git a/src/group-theory/left-quasigroups.lagda.md b/src/group-theory/left-quasigroups.lagda.md
@@ -58,9 +58,13 @@ module _
 
   is-prop-is-left-Quasigroup : is-prop is-left-Quasigroup
   is-prop-is-left-Quasigroup =
-    is-prop-Σ is-prop-is-left-cancellative-left-div (λ _ → is-prop-is-right-cancellative-left-div)
+    is-prop-Σ is-prop-is-left-cancellative-left-div
+      ( λ _ → is-prop-is-right-cancellative-left-div)
 
 left-Quasigroup : (l : Level) → UU (lsuc l)
 left-Quasigroup l =
-  Σ (Set l) (λ Q → Σ (type-Set Q → type-Set Q → type-Set Q) (λ mul → Σ (type-Set Q → type-Set Q → type-Set Q) λ left-div → is-left-Quasigroup Q mul left-div))
+  Σ ( Set l)
+    ( λ Q → Σ (type-Set Q → type-Set Q → type-Set Q)
+    ( λ mul → Σ (type-Set Q → type-Set Q → type-Set Q)
+    ( λ left-div → is-left-Quasigroup Q mul left-div)))
 ```
diff --git a/src/group-theory/right-quasigroups.lagda.md b/src/group-theory/right-quasigroups.lagda.md
@@ -60,9 +60,13 @@ module _
 
   is-prop-is-right-Quasigroup : is-prop is-right-Quasigroup
   is-prop-is-right-Quasigroup =
-    is-prop-Σ is-prop-is-left-cancellative-right-div (λ _ → is-prop-is-right-cancellative-right-div)
+    is-prop-Σ is-prop-is-left-cancellative-right-div
+      ( λ _ → is-prop-is-right-cancellative-right-div)
 
 right-Quasigroup : (l : Level) → UU (lsuc l)
 right-Quasigroup l =
-  Σ (Set l) (λ Q → Σ (type-Set Q → type-Set Q → type-Set Q) (λ mul → Σ (type-Set Q → type-Set Q → type-Set Q) λ right-div → is-right-Quasigroup Q mul right-div))
+  Σ ( Set l)
+    ( λ Q → Σ (type-Set Q → type-Set Q → type-Set Q)
+    ( λ mul → Σ (type-Set Q → type-Set Q → type-Set Q)
+    ( λ right-div → is-right-Quasigroup Q mul right-div)))
 ```