ran pre-commit for cleaning things up. more manual labor to do, however

UniMath · Feb 15, 2025 · 14a7113 · 14a7113
1 parent c1e4699
commit 14a7113
Show file tree

Hide file tree

Showing 4 changed files with 39 additions and 17 deletions.
diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md
@@ -113,7 +113,9 @@ open import group-theory.kernels-homomorphisms-abelian-groups public
 open import group-theory.kernels-homomorphisms-concrete-groups public
 open import group-theory.kernels-homomorphisms-groups public
 open import group-theory.large-semigroups public
+open import group-theory.left-quasigroups public
 open import group-theory.loop-groups-sets public
+open import group-theory.loops public
 open import group-theory.mere-equivalences-concrete-group-actions public
 open import group-theory.mere-equivalences-group-actions public
 open import group-theory.minkowski-multiplication-commutative-monoids public
@@ -158,11 +160,13 @@ open import group-theory.products-of-elements-monoids public
 open import group-theory.products-of-tuples-of-elements-commutative-monoids public
 open import group-theory.pullbacks-subgroups public
 open import group-theory.pullbacks-subsemigroups public
+open import group-theory.quasigroups public
 open import group-theory.quotient-groups public
 open import group-theory.quotient-groups-concrete-groups public
 open import group-theory.quotients-abelian-groups public
 open import group-theory.rational-commutative-monoids public
 open import group-theory.representations-monoids-precategories public
+open import group-theory.right-quasigroups public
 open import group-theory.saturated-congruence-relations-commutative-monoids public
 open import group-theory.saturated-congruence-relations-monoids public
 open import group-theory.semigroups public
@@ -199,6 +203,7 @@ open import group-theory.trivial-concrete-groups public
 open import group-theory.trivial-group-homomorphisms public
 open import group-theory.trivial-groups public
 open import group-theory.trivial-subgroups public
+open import group-theory.units-quasigroups public
 open import group-theory.unordered-tuples-of-elements-commutative-monoids public
 open import group-theory.wild-representations-monoids public
 ```
diff --git a/src/group-theory/left-quasigroups.lagda.md b/src/group-theory/left-quasigroups.lagda.md
@@ -41,20 +41,26 @@ module _
   is-left-cancellative-left-div = (x y : type-Set Q) → y ＝ mul x (left-div x y)
 
   is-prop-is-left-cancellative-left-div : is-prop is-left-cancellative-left-div
-  is-prop-is-left-cancellative-left-div = is-prop-Π (λ x → is-prop-Π (λ y → is-set-type-Set Q y (mul x (left-div x y))))
+  is-prop-is-left-cancellative-left-div =
+    is-prop-Π (λ x → is-prop-Π (λ y → is-set-type-Set Q y (mul x (left-div x y))))
 
   is-right-cancellative-left-div : UU l
   is-right-cancellative-left-div = (x y : type-Set Q) → y ＝ left-div x (mul x y)
 
-  is-prop-is-right-cancellative-left-div : is-prop is-right-cancellative-left-div
-  is-prop-is-right-cancellative-left-div = is-prop-Π (λ x → is-prop-Π (λ y → is-set-type-Set Q y (left-div x (mul x y))))
+  is-prop-is-right-cancellative-left-div :
+    is-prop is-right-cancellative-left-div
+  is-prop-is-right-cancellative-left-div =
+    is-prop-Π (λ x → is-prop-Π (λ y → is-set-type-Set Q y (left-div x (mul x y))))
 
   is-left-Quasigroup : UU l
-  is-left-Quasigroup = is-left-cancellative-left-div × is-right-cancellative-left-div
+  is-left-Quasigroup =
+    is-left-cancellative-left-div × is-right-cancellative-left-div
 
   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-left-Quasigroup =
+    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))
+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))
 ```
diff --git a/src/group-theory/loops.lagda.md b/src/group-theory/loops.lagda.md
@@ -77,7 +77,8 @@ module _
   has-left-unit-Quasigroup =
     Σ (type-Quasigroup Q) λ e → is-left-unit-Quasigroup e
 
-  element-has-left-unit-Quasigroup : has-left-unit-Quasigroup → type-Quasigroup Q
+  element-has-left-unit-Quasigroup :
+    has-left-unit-Quasigroup → type-Quasigroup Q
   element-has-left-unit-Quasigroup (e , _) = e
 
   left-units-agree-Quasigroup :
@@ -128,7 +129,8 @@ module _
   has-right-unit-Quasigroup =
     Σ (type-Quasigroup Q) λ e → is-right-unit-Quasigroup e
 
-  element-has-right-unit-Quasigroup : has-right-unit-Quasigroup → type-Quasigroup Q
+  element-has-right-unit-Quasigroup :
+    has-right-unit-Quasigroup → type-Quasigroup Q
   element-has-right-unit-Quasigroup (e , _) = e
 
   right-units-agree-Quasigroup :

diff --git a/src/group-theory/right-quasigroups.lagda.md b/src/group-theory/right-quasigroups.lagda.md
@@ -37,23 +37,32 @@ module _
   where
 
   is-left-cancellative-right-div : UU l
-  is-left-cancellative-right-div = (x y : type-Set Q) → y ＝ mul (right-div y x) x
+  is-left-cancellative-right-div =
+    (x y : type-Set Q) → y ＝ mul (right-div y x) x
 
-  is-prop-is-left-cancellative-right-div : is-prop is-left-cancellative-right-div
-  is-prop-is-left-cancellative-right-div = is-prop-Π (λ x → is-prop-Π (λ y → is-set-type-Set Q y (mul (right-div y x) x)))
+  is-prop-is-left-cancellative-right-div :
+    is-prop is-left-cancellative-right-div
+  is-prop-is-left-cancellative-right-div =
+    is-prop-Π (λ x → is-prop-Π (λ y → is-set-type-Set Q y (mul (right-div y x) x)))
 
   is-right-cancellative-right-div : UU l
-  is-right-cancellative-right-div = (x y : type-Set Q) → y ＝ right-div (mul y x) x
+  is-right-cancellative-right-div =
+    (x y : type-Set Q) → y ＝ right-div (mul y x) x
 
-  is-prop-is-right-cancellative-right-div : is-prop is-right-cancellative-right-div
-  is-prop-is-right-cancellative-right-div = is-prop-Π (λ x → is-prop-Π (λ y → is-set-type-Set Q y (right-div (mul y x) x)))
+  is-prop-is-right-cancellative-right-div :
+    is-prop is-right-cancellative-right-div
+  is-prop-is-right-cancellative-right-div =
+    is-prop-Π (λ x → is-prop-Π (λ y → is-set-type-Set Q y (right-div (mul y x) x)))
 
   is-right-Quasigroup : UU l
-  is-right-Quasigroup = is-left-cancellative-right-div × is-right-cancellative-right-div
+  is-right-Quasigroup =
+    is-left-cancellative-right-div × is-right-cancellative-right-div
 
   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-right-Quasigroup =
+    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))
+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))
 ```