Refactor library to use λ where (#809)

Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>

CODINGSTYLE.md

@@ -128,6 +128,49 @@ strategic endeavour to ensure the longevity, vitality, and success of the
     a = construction-of-a
   ```
 
+- **Lambda expressions**: When a lambda expression appears as the argument of a
+  function, we always wrap it in parentheses. We do this even if it is the last
+  argument and thus isn't strictly required to be parenthesized. Note that in
+  some rare cases, a lambda expression might appear at the top level. In this
+  case we don't require the lambda expression to be parenthesized.
+
+  There are multiple syntaxes for writing lambda expressions in Agda. Generally,
+  you have the following options:
+
+  1. Regular lambda expressions without pattern matching:
+
+     ```agda
+     λ x → x
+     ```
+
+  2. Pattern matching lambda expressions on record types:
+
+     ```agda
+     λ (x , y) → x
+     ```
+
+     This syntax only applies to record types with $η$-equality.
+
+  3. Pattern matching lambda expressions with `{...}`:
+
+     ```agda
+     λ { (inl x) → ... ; (inr y) → ...}
+     ```
+
+  4. Pattern matching lambda expressions using the `where` keyword:
+
+     ```agda
+     λ where refl → refl
+     ```
+
+  All four syntaxes are in use in the library, although when possible we try to
+  avoid general pattern matching lambdas, i.e. syntaxes 3 and 4. If need be, we
+  prefer pattern matching using the `where` keyword over the `{...}` syntax.
+  Note that whenever syntax 3 or 4 appear in as part of a construction, the
+  definition should be marked as `abstract`. If computation is necessary for a
+  definition that has these syntaxes in them, this suggests the relevant lambda
+  expression(s) deserve to be factored out as separate definitions.
+
 ## Code comments
 
 Given that the files in `agda-unimath` are literate Agda markdown files,

scripts/blank_line_conventions.py

@@ -11,7 +11,6 @@
 open_tag_pattern = re.compile(r'^```\S+\n', flags=re.MULTILINE)
 close_tag_pattern = re.compile(r'\n```$', flags=re.MULTILINE)
 
-
 if __name__ == '__main__':
 
     status = 0
@@ -23,6 +22,10 @@
         output = re.sub(r'[ \t]+$', '', inputText, flags=re.MULTILINE)
         output = re.sub(r'\n(\s*\n){2,}', '\n\n', output)
 
+        # Remove blank lines before a `where`
+        output = re.sub(r'\n(\s*\n)+(\s+)where(\s|$)',
+                        r'\n\2where\3', output, flags=re.MULTILINE)
+
         # # Add blank line after `module ... where`
         # output = re.sub(r'(^([ \t]*)module[\s({][^\n]*\n(\2\s[^\n]*\n)*\2\s([^\n]*[\s)}])?where)\s*\n(?=\s*[^\n\s])', r'\1\n\n',
         #                 output, flags=re.MULTILINE)

src/category-theory/category-of-functors.lagda.md

@@ -82,9 +82,9 @@ module _
         ( ( equiv-iso-functor-natural-isomorphism-Precategory C D F G) ∘e
           ( extensionality-functor-is-category-Precategory
               C D is-category-D F G))
-        ( λ { refl →
-              compute-iso-functor-natural-isomorphism-eq-Precategory
-                C D F G refl})
+        ( λ where
+          refl →
+            compute-iso-functor-natural-isomorphism-eq-Precategory C D F G refl)
 ```
 
 ## Definitions

src/category-theory/category-of-maps-categories.lagda.md

@@ -66,7 +66,8 @@ module _
         ( ( distributive-Π-Σ) ∘e
           ( equiv-Π-equiv-family
             ( λ x →
-              extensionality-obj-Category (D , is-category-D)
+              extensionality-obj-Category
+                ( D , is-category-D)
                 ( obj-map-Precategory C D F x)
                 ( obj-map-Precategory C D G x))))
         ( λ K →
@@ -113,10 +114,9 @@ module _
       is-equiv-htpy-equiv
         ( ( equiv-iso-map-natural-isomorphism-map-Precategory C D F G) ∘e
           ( extensionality-map-is-category-Precategory C D is-category-D F G))
-        ( λ
-          { refl →
-            compute-iso-map-natural-isomorphism-map-eq-Precategory
-              C D F G refl})
+        ( λ where
+          refl →
+            compute-iso-map-natural-isomorphism-map-eq-Precategory C D F G refl)
 ```
 
 ## Definitions

src/category-theory/dependent-products-of-categories.lagda.md

@@ -50,7 +50,7 @@ module _
           equiv-Π-equiv-family
             ( λ i → extensionality-obj-Category (C i) (x i) (y i)) ∘e
           equiv-funext)
-        ( λ {refl → refl})
+        ( λ where refl → refl)
 
   Π-Category : Category (l1 ⊔ l2) (l1 ⊔ l3)
   pr1 Π-Category = Π-Precategory I (precategory-Category ∘ C)

src/category-theory/dependent-products-of-large-categories.lagda.md

@@ -53,7 +53,7 @@ module _
           ( equiv-Π-equiv-family
             ( λ i → extensionality-obj-Large-Category (C i) (x i) (y i))) ∘e
           ( equiv-funext))
-        ( λ {refl → refl})
+        ( λ where refl → refl)
 
   Π-Large-Category : Large-Category (λ l2 → l1 ⊔ α l2) (λ l2 l3 → l1 ⊔ β l2 l3)
   large-precategory-Large-Category

src/commutative-algebra/products-ideals-commutative-rings.lagda.md

@@ -170,25 +170,28 @@ module _
   (S : subset-Commutative-Ring l2 A) (T : subset-Commutative-Ring l3 A)
   where
 
-  forward-inclusion-preserves-product-ideal-subset-Commutative-Ring :
-    leq-ideal-Commutative-Ring A
-      ( ideal-subset-Commutative-Ring A (product-subset-Commutative-Ring A S T))
-      ( product-ideal-Commutative-Ring A
-        ( ideal-subset-Commutative-Ring A S)
-        ( ideal-subset-Commutative-Ring A T))
-  forward-inclusion-preserves-product-ideal-subset-Commutative-Ring =
-    is-ideal-generated-by-subset-ideal-subset-Commutative-Ring A
-      ( product-subset-Commutative-Ring A S T)
-      ( product-ideal-Commutative-Ring A
-        ( ideal-subset-Commutative-Ring A S)
-        ( ideal-subset-Commutative-Ring A T))
-      ( λ x H →
-        apply-universal-property-trunc-Prop H
-          ( subset-product-ideal-Commutative-Ring A
-            ( ideal-subset-Commutative-Ring A S)
-            ( ideal-subset-Commutative-Ring A T)
-            ( x))
-          ( λ { (s , t , refl) →
+  abstract
+    forward-inclusion-preserves-product-ideal-subset-Commutative-Ring :
+      leq-ideal-Commutative-Ring A
+        ( ideal-subset-Commutative-Ring A
+          ( product-subset-Commutative-Ring A S T))
+        ( product-ideal-Commutative-Ring A
+          ( ideal-subset-Commutative-Ring A S)
+          ( ideal-subset-Commutative-Ring A T))
+    forward-inclusion-preserves-product-ideal-subset-Commutative-Ring =
+      is-ideal-generated-by-subset-ideal-subset-Commutative-Ring A
+        ( product-subset-Commutative-Ring A S T)
+        ( product-ideal-Commutative-Ring A
+          ( ideal-subset-Commutative-Ring A S)
+          ( ideal-subset-Commutative-Ring A T))
+        ( λ x H →
+          apply-universal-property-trunc-Prop H
+            ( subset-product-ideal-Commutative-Ring A
+              ( ideal-subset-Commutative-Ring A S)
+              ( ideal-subset-Commutative-Ring A T)
+              ( x))
+            ( λ where
+              ( s , t , refl) →
                 contains-product-product-ideal-Commutative-Ring A
                   ( ideal-subset-Commutative-Ring A S)
                   ( ideal-subset-Commutative-Ring A T)
@@ -199,7 +202,7 @@ module _
                     ( pr2 s))
                   ( contains-subset-ideal-subset-Commutative-Ring A T
                     ( pr1 t)
-                    ( pr2 t))}))
+                    ( pr2 t))))
 
   left-backward-inclusion-preserves-product-ideal-subset-Commutative-Ring :
     {x s y : type-Commutative-Ring A} →

src/elementary-number-theory/dirichlet-convolution.lagda.md

@@ -39,8 +39,8 @@ module _
     bounded-sum-arithmetic-function-Ring R
       ( succ-ℕ n)
       ( λ x → div-ℕ-Decidable-Prop (pr1 x) (succ-ℕ n) (pr2 x))
-      ( λ { (pair x K) H →
-            mul-Ring R
-              ( f ( pair x K))
-              ( g ( quotient-div-nonzero-ℕ x (succ-nonzero-ℕ' n) H))})
+      ( λ (x , K) H →
+        mul-Ring R
+          ( f ( pair x K))
+          ( g ( quotient-div-nonzero-ℕ x (succ-nonzero-ℕ' n) H)))
 ```

src/elementary-number-theory/divisibility-integers.lagda.md

@@ -482,7 +482,7 @@ is-zero-sim-unit-ℤ {x} {y} H p =
     ( λ g → g (inv (β g) ∙ (ap ((u g) *ℤ_) p ∙ right-zero-law-mul-ℤ (u g))))
   where
   K : is-nonzero-ℤ y → presim-unit-ℤ x y
-  K g = H (λ {(pair u v) → g v})
+  K g = H (λ (u , v) → g v)
   u : is-nonzero-ℤ y → ℤ
   u g = pr1 (pr1 (K g))
   v : is-nonzero-ℤ y → ℤ
@@ -547,8 +547,8 @@ transitive-presim-unit-ℤ x y z (pair (pair v K) q) (pair (pair u H) p) =
 transitive-sim-unit-ℤ : is-transitive sim-unit-ℤ
 transitive-sim-unit-ℤ x y z K H f =
   transitive-presim-unit-ℤ x y z
-    ( K (λ {(p , q) → f (is-zero-sim-unit-ℤ' H p , q)}))
-    ( H (λ {(p , q) → f (p , is-zero-sim-unit-ℤ K q)}))
+    ( K (λ (p , q) → f (is-zero-sim-unit-ℤ' H p , q)))
+    ( H (λ (p , q) → f (p , is-zero-sim-unit-ℤ K q)))
 ```
 
 ### `sim-unit-ℤ x y` holds if and only if `x|y` and `y|x`

src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md

@@ -307,14 +307,15 @@ is-minimal-least-nontrivial-divisor-ℕ n H x K d =
 ### The least nontrivial divisor of a number `> 1` is nonzero
 
 ```agda
-is-nonzero-least-nontrivial-divisor-ℕ :
-  (n : ℕ) (H : le-ℕ 1 n) → is-nonzero-ℕ (nat-least-nontrivial-divisor-ℕ n H)
-is-nonzero-least-nontrivial-divisor-ℕ n H =
-  is-nonzero-div-ℕ
-    ( nat-least-nontrivial-divisor-ℕ n H)
-    ( n)
-    ( div-least-nontrivial-divisor-ℕ n H)
-    ( λ { refl → H})
+abstract
+  is-nonzero-least-nontrivial-divisor-ℕ :
+    (n : ℕ) (H : le-ℕ 1 n) → is-nonzero-ℕ (nat-least-nontrivial-divisor-ℕ n H)
+  is-nonzero-least-nontrivial-divisor-ℕ n H =
+    is-nonzero-div-ℕ
+      ( nat-least-nontrivial-divisor-ℕ n H)
+      ( n)
+      ( div-least-nontrivial-divisor-ℕ n H)
+      ( λ where refl → H)
 ```
 
 ### The least nontrivial divisor of a number `> 1` is prime

src/elementary-number-theory/powers-of-two.lagda.md

@@ -55,49 +55,51 @@ is-nonzero-pair-expansion u v =
     ( is-nonzero-exp-ℕ 2 u is-nonzero-two-ℕ)
     ( is-nonzero-succ-ℕ _)
 
-has-pair-expansion-is-even-or-odd :
-  (n : ℕ) → is-even-ℕ n + is-odd-ℕ n → pair-expansion n
-has-pair-expansion-is-even-or-odd n =
-  strong-ind-ℕ
-  ( λ m → (is-even-ℕ m + is-odd-ℕ m) → (pair-expansion m))
-  ( λ x → (0 , 0) , refl)
-  ( λ k f →
-    ( λ {
-      ( inl x) →
-        ( let s = has-odd-expansion-is-odd k (is-odd-is-even-succ-ℕ k x)
-          in pair
-            ( 0 , (succ-ℕ (pr1 s)))
-            ( ( ap ((succ-ℕ ∘ succ-ℕ) ∘ succ-ℕ) (left-unit-law-add-ℕ _)) ∙
-            ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 s))))) ;
-      ( inr x) →
-        ( let e : is-even-ℕ k
-              e = is-even-is-odd-succ-ℕ k x
-
-              t : (pr1 e) ≤-ℕ k
-              t = leq-quotient-div-ℕ' 2 k is-nonzero-two-ℕ e
-
-              s : (pair-expansion (pr1 e))
-              s = f (pr1 e) t (is-decidable-is-even-ℕ (pr1 e))
-          in
-            pair
-              ( succ-ℕ (pr1 (pr1 s)) , pr2 (pr1 s))
-              ( ( ap
-                  ( _*ℕ (succ-ℕ ((pr2 (pr1 s)) *ℕ 2)))
-                  ( commutative-mul-ℕ (exp-ℕ 2 (pr1 (pr1 s))) 2)) ∙
-                ( ( associative-mul-ℕ 2
-                    ( exp-ℕ 2 (pr1 (pr1 s)))
-                    ( succ-ℕ ((pr2 (pr1 s)) *ℕ 2))) ∙
-                  ( ( ap (2 *ℕ_) (pr2 s)) ∙
-                    ( ( ap succ-ℕ
-                        ( left-successor-law-add-ℕ (0 +ℕ (pr1 e)) (pr1 e))) ∙
-                      ( ( ap
-                          ( succ-ℕ ∘ succ-ℕ)
-                          ( ap (_+ℕ (pr1 e)) (left-unit-law-add-ℕ (pr1 e)))) ∙
+abstract
+  has-pair-expansion-is-even-or-odd :
+    (n : ℕ) → is-even-ℕ n + is-odd-ℕ n → pair-expansion n
+  has-pair-expansion-is-even-or-odd n =
+    strong-ind-ℕ
+    ( λ m → (is-even-ℕ m + is-odd-ℕ m) → (pair-expansion m))
+    ( λ x → (0 , 0) , refl)
+    ( λ k f →
+      ( λ where
+        ( inl x) →
+          ( let s = has-odd-expansion-is-odd k (is-odd-is-even-succ-ℕ k x)
+            in
+              pair
+                ( 0 , (succ-ℕ (pr1 s)))
+                ( ( ap ((succ-ℕ ∘ succ-ℕ) ∘ succ-ℕ) (left-unit-law-add-ℕ _)) ∙
+                  ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 s)))))
+        ( inr x) →
+          ( let e : is-even-ℕ k
+                e = is-even-is-odd-succ-ℕ k x
+
+                t : (pr1 e) ≤-ℕ k
+                t = leq-quotient-div-ℕ' 2 k is-nonzero-two-ℕ e
+
+                s : (pair-expansion (pr1 e))
+                s = f (pr1 e) t (is-decidable-is-even-ℕ (pr1 e))
+            in
+              pair
+                ( succ-ℕ (pr1 (pr1 s)) , pr2 (pr1 s))
+                ( ( ap
+                    ( _*ℕ (succ-ℕ ((pr2 (pr1 s)) *ℕ 2)))
+                    ( commutative-mul-ℕ (exp-ℕ 2 (pr1 (pr1 s))) 2)) ∙
+                  ( ( associative-mul-ℕ 2
+                      ( exp-ℕ 2 (pr1 (pr1 s)))
+                      ( succ-ℕ ((pr2 (pr1 s)) *ℕ 2))) ∙
+                    ( ( ap (2 *ℕ_) (pr2 s)) ∙
+                      ( ( ap succ-ℕ
+                          ( left-successor-law-add-ℕ (0 +ℕ (pr1 e)) (pr1 e))) ∙
                         ( ( ap
                             ( succ-ℕ ∘ succ-ℕ)
-                            ( inv (right-two-law-mul-ℕ (pr1 e)))) ∙
-                            ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 e))))))))))}))
-  ( n)
+                            ( ap (_+ℕ (pr1 e)) (left-unit-law-add-ℕ (pr1 e)))) ∙
+                          ( ( ap
+                              ( succ-ℕ ∘ succ-ℕ)
+                              ( inv (right-two-law-mul-ℕ (pr1 e)))) ∙
+                              ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 e))))))))))))
+    ( n)
 
 has-pair-expansion : (n : ℕ) → pair-expansion n
 has-pair-expansion n =

src/finite-group-theory/concrete-quaternion-group.lagda.md

@@ -12,11 +12,11 @@ open import elementary-number-theory.natural-numbers
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
-open import foundation.isolated-points
+open import foundation.isolated-elements
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
-open import univalent-combinatorics.complements-isolated-points
+open import univalent-combinatorics.complements-isolated-elements
 open import univalent-combinatorics.cubes
 open import univalent-combinatorics.equality-finite-types
 open import univalent-combinatorics.equivalences-cubes
@@ -37,7 +37,7 @@ equiv-face-cube :
       ( map-axis-equiv-cube (succ-ℕ k) X Y e d a))
 equiv-face-cube k X Y e d a =
   pair
-    ( equiv-complement-point-UU-Fin k
+    ( equiv-complement-element-UU-Fin k
       ( pair (dim-cube-UU-Fin (succ-ℕ k) X) d)
       ( pair
         ( dim-cube-UU-Fin (succ-ℕ k) Y)
@@ -48,7 +48,7 @@ equiv-face-cube k X Y e d a =
       ( equiv-tr
         ( axis-cube (succ-ℕ k) Y)
         ( inv
-          ( natural-inclusion-equiv-complement-isolated-point
+          ( natural-inclusion-equiv-complement-isolated-element
             ( dim-equiv-cube (succ-ℕ k) X Y e)
             ( pair d
               ( λ z →
@@ -68,7 +68,7 @@ equiv-face-cube k X Y e d a =
             ( refl)
             ( d')))) ∘e
       ( axis-equiv-cube (succ-ℕ k) X Y e
-        ( inclusion-complement-point-UU-Fin k
+        ( inclusion-complement-element-UU-Fin k
           ( pair (dim-cube-UU-Fin (succ-ℕ k) X) d) d')))
 
 cube-with-labeled-faces :