getting below the char limit per line

UniMath · Feb 15, 2025 · b8996f9 · b8996f9
1 parent ab268fa
commit b8996f9
Show file tree

Hide file tree

Showing 3 changed files with 135 additions and 62 deletions.
diff --git a/src/quasigroups.lagda.md b/src/quasigroups.lagda.md
@@ -0,0 +1,8 @@
+# Quasigroups
+
+```agda
+module quasigroups where
+
+open import quasigroups.loops public
+open import quasigroups.quasigroups public
+```
diff --git a/src/quasigroups/loops.lagda.md b/src/quasigroups/loops.lagda.md
@@ -18,14 +18,9 @@ open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
+open import foundation-core.contractible-types
 open import foundation-core.dependent-identifications
-open import foundation-core.equality-dependent-pair-types
-open import foundation-core.propositions
-open import foundation-core.sets
 open import foundation-core.subtypes
-open import foundation-core.transport-along-identifications
-
-open import foundation-core.contractible-types
 
 open import quasigroups.quasigroups
 ```
@@ -68,20 +63,27 @@ module _
   is-left-unit-Quasigroup : (e : type-Quasigroup Q) → UU l
   is-left-unit-Quasigroup e = (x : type-Quasigroup Q) → e * x ＝ x
 
-  is-prop-is-left-unit-Quasigroup : (e : type-Quasigroup Q) → is-prop (is-left-unit-Quasigroup e)
-  is-prop-is-left-unit-Quasigroup e = is-prop-Π (λ x → is-set-Quasigroup Q (e * x) x)
+  is-prop-is-left-unit-Quasigroup :
+    (e : type-Quasigroup Q) → is-prop (is-left-unit-Quasigroup e)
+  is-prop-is-left-unit-Quasigroup e =
+    is-prop-Π (λ x → is-set-Quasigroup Q (e * x) x)
 
   is-left-unit-Quasigroup-Prop : (e : type-Quasigroup Q) → Prop l
-  is-left-unit-Quasigroup-Prop e = is-left-unit-Quasigroup e , is-prop-is-left-unit-Quasigroup e
+  is-left-unit-Quasigroup-Prop e =
+    is-left-unit-Quasigroup e , is-prop-is-left-unit-Quasigroup e
 
   has-left-unit-Quasigroup : UU l
-  has-left-unit-Quasigroup = Σ (type-Quasigroup Q) λ e → is-left-unit-Quasigroup e
+  has-left-unit-Quasigroup =
+    Σ (type-Quasigroup Q) λ e → is-left-unit-Quasigroup e
 
   term-has-left-unit-Quasigroup : has-left-unit-Quasigroup → type-Quasigroup Q
   term-has-left-unit-Quasigroup (e , _) = e
 
-  left-units-agree-Quasigroup : (e f : has-left-unit-Quasigroup) → term-has-left-unit-Quasigroup e ＝ term-has-left-unit-Quasigroup f
-  left-units-agree-Quasigroup (e , e-left-unit) (f , f-left-unit) = equational-reasoning
+  left-units-agree-Quasigroup :
+    (e f : has-left-unit-Quasigroup) → term-has-left-unit-Quasigroup e
+    ＝ term-has-left-unit-Quasigroup f
+  left-units-agree-Quasigroup (e , e-left-unit) (f , f-left-unit) =
+    equational-reasoning
     e ＝ (e * f) r/ f
       by is-right-cancellative-right-div-Quasigroup Q f e
     ＝ f r/ f
@@ -92,8 +94,12 @@ module _
       by inv (is-right-cancellative-right-div-Quasigroup Q f f)
 
   is-prop-has-left-unit-Quasigroup : is-prop has-left-unit-Quasigroup
-  pr1 (is-prop-has-left-unit-Quasigroup e f) = eq-type-subtype is-left-unit-Quasigroup-Prop (left-units-agree-Quasigroup e f)
-  pr2 (is-prop-has-left-unit-Quasigroup e f) p = is-set-has-uip (is-set-type-subtype is-left-unit-Quasigroup-Prop (is-set-Quasigroup Q)) e f (pr1 (is-prop-has-left-unit-Quasigroup e f)) p
+  pr1 (is-prop-has-left-unit-Quasigroup e f) =
+    eq-type-subtype is-left-unit-Quasigroup-Prop
+    (left-units-agree-Quasigroup e f)
+  pr2 (is-prop-has-left-unit-Quasigroup e f) p =
+    is-set-has-uip (is-set-type-subtype is-left-unit-Quasigroup-Prop
+    (is-set-Quasigroup Q)) e f (pr1 (is-prop-has-left-unit-Quasigroup e f)) p
 ```
 
 ### Right units in quasigroups
@@ -102,20 +108,27 @@ module _
   is-right-unit-Quasigroup : (e : type-Quasigroup Q) → UU l
   is-right-unit-Quasigroup e = (x : type-Quasigroup Q) → x * e ＝ x
 
-  is-prop-is-right-unit-Quasigroup : (e : type-Quasigroup Q) → is-prop (is-right-unit-Quasigroup e)
-  is-prop-is-right-unit-Quasigroup e = is-prop-Π (λ x → is-set-Quasigroup Q (x * e) x)
+  is-prop-is-right-unit-Quasigroup :
+    (e : type-Quasigroup Q) → is-prop (is-right-unit-Quasigroup e)
+  is-prop-is-right-unit-Quasigroup e =
+    is-prop-Π (λ x → is-set-Quasigroup Q (x * e) x)
 
   is-right-unit-Quasigroup-Prop : (e : type-Quasigroup Q) → Prop l
-  is-right-unit-Quasigroup-Prop e = is-right-unit-Quasigroup e , is-prop-is-right-unit-Quasigroup e
+  is-right-unit-Quasigroup-Prop e =
+    is-right-unit-Quasigroup e , is-prop-is-right-unit-Quasigroup e
 
   has-right-unit-Quasigroup : UU l
-  has-right-unit-Quasigroup = Σ (type-Quasigroup Q) λ e → is-right-unit-Quasigroup e
+  has-right-unit-Quasigroup =
+    Σ (type-Quasigroup Q) λ e → is-right-unit-Quasigroup e
 
   term-has-right-unit-Quasigroup : has-right-unit-Quasigroup → type-Quasigroup Q
   term-has-right-unit-Quasigroup (e , _) = e
 
-  right-units-agree-Quasigroup : (e f : has-right-unit-Quasigroup) → term-has-right-unit-Quasigroup e ＝ term-has-right-unit-Quasigroup f
-  right-units-agree-Quasigroup (e , e-right-unit) (f , f-right-unit) = equational-reasoning
+  right-units-agree-Quasigroup :
+    (e f : has-right-unit-Quasigroup) → term-has-right-unit-Quasigroup e
+    ＝ term-has-right-unit-Quasigroup f
+  right-units-agree-Quasigroup (e , e-right-unit) (f , f-right-unit) =
+    equational-reasoning
     e ＝ f l/ (f * e)
       by is-right-cancellative-left-div-Quasigroup Q f e
     ＝ f l/ f
@@ -126,8 +139,12 @@ module _
       by inv (is-right-cancellative-left-div-Quasigroup Q f f)
 
   is-prop-has-right-unit-Quasigroup : is-prop has-right-unit-Quasigroup
-  pr1 (is-prop-has-right-unit-Quasigroup e f) = eq-type-subtype is-right-unit-Quasigroup-Prop (right-units-agree-Quasigroup e f)
-  pr2 (is-prop-has-right-unit-Quasigroup e f) p = is-set-has-uip (is-set-type-subtype is-right-unit-Quasigroup-Prop (is-set-Quasigroup Q)) e f (pr1 (is-prop-has-right-unit-Quasigroup e f)) p
+  pr1 (is-prop-has-right-unit-Quasigroup e f) =
+    eq-type-subtype is-right-unit-Quasigroup-Prop
+    (right-units-agree-Quasigroup e f)
+  pr2 (is-prop-has-right-unit-Quasigroup e f) p =
+    is-set-has-uip (is-set-type-subtype is-right-unit-Quasigroup-Prop
+    (is-set-Quasigroup Q)) e f (pr1 (is-prop-has-right-unit-Quasigroup e f)) p
 ```
 
 ### Units in quasigroups
@@ -138,22 +155,32 @@ type of units is equivalent to the type of pairs of left and right units.
 
 ```agda
   has-unit-Quasigroup : UU l
-  has-unit-Quasigroup = Σ (type-Quasigroup Q) λ e → is-left-unit-Quasigroup e × is-right-unit-Quasigroup e
+  has-unit-Quasigroup =
+    Σ (type-Quasigroup Q)
+    λ e → is-left-unit-Quasigroup e × is-right-unit-Quasigroup e
 
   unit-has-unit-Quasigroup : has-unit-Quasigroup → type-Quasigroup Q
   unit-has-unit-Quasigroup (e , _) = e
 
-  has-unit-has-left-unit-Quasigroup : has-unit-Quasigroup → has-left-unit-Quasigroup
+  has-unit-has-left-unit-Quasigroup :
+    has-unit-Quasigroup → has-left-unit-Quasigroup
   has-unit-has-left-unit-Quasigroup (e , e-left-unit , _) = e , e-left-unit
 
-  has-unit-has-right-unit-Quasigroup : has-unit-Quasigroup → has-right-unit-Quasigroup
+  has-unit-has-right-unit-Quasigroup :
+    has-unit-Quasigroup → has-right-unit-Quasigroup
   has-unit-has-right-unit-Quasigroup (e , _ , e-right-unit) = e , e-right-unit
 
-  has-unit-has-left-and-right-units-Quasigroup : has-unit-Quasigroup → has-left-unit-Quasigroup × has-right-unit-Quasigroup
-  has-unit-has-left-and-right-units-Quasigroup e = (has-unit-has-left-unit-Quasigroup e) , (has-unit-has-right-unit-Quasigroup e)
-
-  left-and-right-units-agree-Quasigroup : (e : has-left-unit-Quasigroup) → (f : has-right-unit-Quasigroup) → term-has-left-unit-Quasigroup e ＝ term-has-right-unit-Quasigroup f
-  left-and-right-units-agree-Quasigroup (e , e-left-unit) (f , f-right-unit) = equational-reasoning
+  has-unit-has-left-and-right-units-Quasigroup :
+    has-unit-Quasigroup → has-left-unit-Quasigroup × has-right-unit-Quasigroup
+  has-unit-has-left-and-right-units-Quasigroup e =
+    (has-unit-has-left-unit-Quasigroup e) ,
+    (has-unit-has-right-unit-Quasigroup e)
+
+  left-and-right-units-agree-Quasigroup :
+    (e : has-left-unit-Quasigroup) → (f : has-right-unit-Quasigroup) →
+    term-has-left-unit-Quasigroup e ＝ term-has-right-unit-Quasigroup f
+  left-and-right-units-agree-Quasigroup (e , e-left-unit) (f , f-right-unit) =
+    equational-reasoning
     e ＝ (e * f) r/ f
       by is-right-cancellative-right-div-Quasigroup Q f e
     ＝ f r/ f
@@ -163,13 +190,20 @@ type of units is equivalent to the type of pairs of left and right units.
     ＝ f
       by inv (is-right-cancellative-right-div-Quasigroup Q f f)
 
-  has-left-and-right-units-is-left-unit-is-right-unit : (e : has-left-unit-Quasigroup) → has-right-unit-Quasigroup → is-right-unit-Quasigroup (term-has-left-unit-Quasigroup e)
-  has-left-and-right-units-is-left-unit-is-right-unit e f x = inv-tr is-right-unit-Quasigroup (left-and-right-units-agree-Quasigroup e f) (pr2 f) x
+  has-left-and-right-units-is-left-unit-is-right-unit :
+    (e : has-left-unit-Quasigroup) → has-right-unit-Quasigroup →
+    is-right-unit-Quasigroup (term-has-left-unit-Quasigroup e)
+  has-left-and-right-units-is-left-unit-is-right-unit e f x =
+    inv-tr is-right-unit-Quasigroup (left-and-right-units-agree-Quasigroup e f)
+    (pr2 f) x
 
-  has-left-and-right-units-has-unit-Quasigroup : has-left-unit-Quasigroup → has-right-unit-Quasigroup → has-unit-Quasigroup
+  has-left-and-right-units-has-unit-Quasigroup :
+    has-left-unit-Quasigroup → has-right-unit-Quasigroup → has-unit-Quasigroup
   pr1 (has-left-and-right-units-has-unit-Quasigroup (e , _) _) = e
-  pr1 (pr2 (has-left-and-right-units-has-unit-Quasigroup (e , e-left-unit) _)) = e-left-unit
-  pr2 (pr2 (has-left-and-right-units-has-unit-Quasigroup e f)) = has-left-and-right-units-is-left-unit-is-right-unit e f
+  pr1 (pr2 (has-left-and-right-units-has-unit-Quasigroup (e , e-left-unit) _)) =
+    e-left-unit
+  pr2 (pr2 (has-left-and-right-units-has-unit-Quasigroup e f)) =
+    has-left-and-right-units-is-left-unit-is-right-unit e f
 ```
 
 ### Loops

diff --git a/src/quasigroups/quasigroups.lagda.md b/src/quasigroups/quasigroups.lagda.md
@@ -1,22 +1,18 @@
 # Quasigroups
 
 ```agda
-
 module quasigroups.quasigroups where
-
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
-
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
-
 ```
 
 </details>
@@ -66,22 +62,32 @@ module _
   is-left-cancellative-left-div = (x y : Q') → y ＝ (x * (x l/ 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 → Q'-is-set y (x * (x l/ y)))
+  is-prop-is-left-cancellative-left-div =
+    is-prop-Π λ x → is-prop-Π (λ y → Q'-is-set y (x * (x l/ y)))
 
   is-right-cancellative-left-div : UU l
   is-right-cancellative-left-div = (x y : Q') → y ＝ (x l/ (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 → Q'-is-set y (x l/ (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 → Q'-is-set y (x l/ (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-cancellative-left-div Q mul left-div × is-right-cancellative-left-div 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-cancellative-left-div Q mul left-div ×
+  is-right-cancellative-left-div Q mul left-div))
 ```
 
 #### Right quasigroups
@@ -108,23 +114,33 @@ module _
   is-left-cancellative-right-div : UU l
   is-left-cancellative-right-div = (x y : Q') → y ＝ ((y r/ 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 → Q'-is-set y ((y r/ 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 → Q'-is-set y ((y r/ x) * x))
 
   is-right-cancellative-right-div : UU l
   is-right-cancellative-right-div = (x y : Q') → y ＝ ((y * x) r/ 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 → Q'-is-set y ((y * x) r/ 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 → Q'-is-set y ((y * x) r/ 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))
 ```
 
 #### Quasigroups
@@ -134,7 +150,11 @@ multiplication.
 
 ```agda
 Quasigroup : (l : Level) → UU (lsuc l)
-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 → Σ (type-Set Q → type-Set Q → type-Set Q) (λ right-div → is-left-Quasigroup Q mul left-div × is-right-Quasigroup Q mul right-div)))
+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 → Σ (type-Set Q → type-Set Q → type-Set Q) (λ right-div →
+  is-left-Quasigroup Q mul left-div × is-right-Quasigroup Q mul right-div)))
 
 module _
   {l : Level} (Q : Quasigroup l)
@@ -158,17 +178,28 @@ module _
   right-div-Quasigroup : type-Quasigroup → type-Quasigroup → type-Quasigroup
   right-div-Quasigroup = pr1 (pr2 (pr2 (pr2 Q)))
 
-  is-left-cancellative-left-div-Quasigroup : is-left-cancellative-left-div set-Quasigroup mul-Quasigroup left-div-Quasigroup
+  is-left-cancellative-left-div-Quasigroup :
+    is-left-cancellative-left-div set-Quasigroup
+    mul-Quasigroup left-div-Quasigroup
   is-left-cancellative-left-div-Quasigroup = pr1 (pr1 (pr2 (pr2 (pr2 (pr2 Q)))))
 
-  is-right-cancellative-left-div-Quasigroup : is-right-cancellative-left-div set-Quasigroup mul-Quasigroup left-div-Quasigroup
-  is-right-cancellative-left-div-Quasigroup = pr2 (pr1 (pr2 (pr2 (pr2 (pr2 Q)))))
-
-  is-left-cancellative-right-div-Quasigroup : is-left-cancellative-right-div set-Quasigroup mul-Quasigroup right-div-Quasigroup
-  is-left-cancellative-right-div-Quasigroup = pr1 (pr2 (pr2 (pr2 (pr2 (pr2 Q)))))
-
-  is-right-cancellative-right-div-Quasigroup : is-right-cancellative-right-div set-Quasigroup mul-Quasigroup right-div-Quasigroup
-  is-right-cancellative-right-div-Quasigroup = pr2 (pr2 (pr2 (pr2 (pr2 (pr2 Q)))))
+  is-right-cancellative-left-div-Quasigroup :
+    is-right-cancellative-left-div set-Quasigroup
+    mul-Quasigroup left-div-Quasigroup
+  is-right-cancellative-left-div-Quasigroup =
+    pr2 (pr1 (pr2 (pr2 (pr2 (pr2 Q)))))
+
+  is-left-cancellative-right-div-Quasigroup :
+    is-left-cancellative-right-div set-Quasigroup
+    mul-Quasigroup right-div-Quasigroup
+  is-left-cancellative-right-div-Quasigroup =
+    pr1 (pr2 (pr2 (pr2 (pr2 (pr2 Q)))))
+
+  is-right-cancellative-right-div-Quasigroup :
+    is-right-cancellative-right-div set-Quasigroup
+    mul-Quasigroup right-div-Quasigroup
+  is-right-cancellative-right-div-Quasigroup =
+    pr2 (pr2 (pr2 (pr2 (pr2 (pr2 Q)))))
 ```
 
 ## External links