Refactor library to use λ where

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

@@ -188,18 +188,19 @@ module _
             ( ideal-subset-Commutative-Ring A S)
             ( ideal-subset-Commutative-Ring A T)
             ( x))
-          ( λ { (s , t , refl) →
-                contains-product-product-ideal-Commutative-Ring A
-                  ( ideal-subset-Commutative-Ring A S)
-                  ( ideal-subset-Commutative-Ring A T)
+          ( λ where
+            ( s , t , refl) →
+              contains-product-product-ideal-Commutative-Ring A
+                ( ideal-subset-Commutative-Ring A S)
+                ( ideal-subset-Commutative-Ring A T)
+                ( pr1 s)
+                ( pr1 t)
+                ( contains-subset-ideal-subset-Commutative-Ring A S
                   ( pr1 s)
+                  ( pr2 s))
+                ( contains-subset-ideal-subset-Commutative-Ring A T
                   ( pr1 t)
-                  ( contains-subset-ideal-subset-Commutative-Ring A S
-                    ( pr1 s)
-                    ( 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

@@ -314,7 +314,7 @@ is-nonzero-least-nontrivial-divisor-ℕ n H =
     ( nat-least-nontrivial-divisor-ℕ n H)
     ( n)
     ( div-least-nontrivial-divisor-ℕ n H)
-    ( λ { refl → H})
+    ( λ where refl → H)
 ```
 
 ### The least nontrivial divisor of a number `> 1` is prime

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

@@ -62,13 +62,13 @@ has-pair-expansion-is-even-or-odd n =
   ( λ 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))))) ;
+              ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 s)))))
       ( inr x) →
         ( let e : is-even-ℕ k
               e = is-even-is-odd-succ-ℕ k x
@@ -96,7 +96,7 @@ has-pair-expansion-is-even-or-odd n =
                         ( ( ap
                             ( succ-ℕ ∘ succ-ℕ)
                             ( inv (right-two-law-mul-ℕ (pr1 e)))) ∙
-                            ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 e))))))))))}))
+                            ( ( ap (succ-ℕ ∘ succ-ℕ) (pr2 e))))))))))))
   ( n)
 
 has-pair-expansion : (n : ℕ) → pair-expansion n

src/finite-group-theory/orbits-permutations.lagda.md

@@ -463,12 +463,11 @@ module _
         apply-universal-property-trunc-Prop
           ( Q)
           ( pr1 same-orbits-permutation a c)
-          ( λ { (k2 , q) →
-                ( unit-trunc-Prop
-                  ( pair
-                    ( k2 +ℕ k1)
-                    ( (iterate-add-ℕ k2 k1 (map-equiv f) a) ∙
-                      ( ap (iterate k2 (map-equiv f)) p ∙ q))))}))
+          ( λ (k2 , q) →
+            ( unit-trunc-Prop
+              ( ( k2 +ℕ k1) ,
+                ( (iterate-add-ℕ k2 k1 (map-equiv f) a) ∙
+                  ( ap (iterate k2 (map-equiv f)) p ∙ q))))))
 
   abstract
     is-decidable-same-orbits-permutation :
@@ -1126,23 +1125,25 @@ module _
             (λ pa → lemma2 g (pair (pr1 pa) (inl (pr2 pa)))))
         ( is-equiv-is-prop is-prop-type-trunc-Prop
           ( is-prop-type-Prop (coprod-sim-Equivalence-Relation-a-b-Prop g P x))
-          ( λ {
-            (inl T) →
-            apply-universal-property-trunc-Prop T
-              ( prop-Equivalence-Relation (same-orbits-permutation-count g) x a)
-              ( λ pa →
-                lemma3
-                  ( lemma2
-                    ( composition-transposition-a-b g)
-                    ( pair (pr1 pa) (inl (pr2 pa))))) ;
-            (inr T) →
-            apply-universal-property-trunc-Prop T
-              ( prop-Equivalence-Relation (same-orbits-permutation-count g) x a)
-              ( λ pa →
-                lemma3
-                  ( lemma2
-                    ( composition-transposition-a-b g)
-                    ( pair (pr1 pa) (inr (pr2 pa)))))}))
+          ( λ where
+            ( inl T) →
+              apply-universal-property-trunc-Prop T
+                ( prop-Equivalence-Relation
+                  ( same-orbits-permutation-count g) x a)
+                ( λ pa →
+                  lemma3
+                    ( lemma2
+                      ( composition-transposition-a-b g)
+                      ( pair (pr1 pa) (inl (pr2 pa)))))
+            ( inr T) →
+              apply-universal-property-trunc-Prop T
+                ( prop-Equivalence-Relation
+                  ( same-orbits-permutation-count g) x a)
+                ( λ pa →
+                  lemma3
+                    ( lemma2
+                      ( composition-transposition-a-b g)
+                      ( (pr1 pa) , (inr (pr2 pa)))))))
       where
       minimal-element-iterate-2-a-b :
         ( g : X ≃ X) →
@@ -1170,17 +1171,18 @@ module _
       equal-iterate-transposition-same-orbits g pa k ineq =
         equal-iterate-transposition x g
           ( λ k' → le-ℕ k' (pr1 (minimal-element-iterate-2-a-b g pa)))
-          ( λ k' p → pair
-            ( λ q →
-              contradiction-le-ℕ k'
-                ( pr1 (minimal-element-iterate-2-a-b g pa))
-                ( p)
-                ( pr2 (pr2 (minimal-element-iterate-2-a-b g pa)) k' (inl q)))
-            ( λ r →
-              contradiction-le-ℕ k'
-                ( pr1 (minimal-element-iterate-2-a-b g pa))
-                ( p)
-                ( pr2 (pr2 (minimal-element-iterate-2-a-b g pa)) k' (inr r))))
+          ( λ k' p →
+            pair
+              ( λ q →
+                contradiction-le-ℕ k'
+                  ( pr1 (minimal-element-iterate-2-a-b g pa))
+                  ( p)
+                  ( pr2 (pr2 (minimal-element-iterate-2-a-b g pa)) k' (inl q)))
+              ( λ r →
+                contradiction-le-ℕ k'
+                  ( pr1 (minimal-element-iterate-2-a-b g pa))
+                  ( p)
+                  ( pr2 (pr2 (minimal-element-iterate-2-a-b g pa)) k' (inr r))))
           ( λ k' ineq' _ →
             transitive-le-ℕ k'
               ( succ-ℕ k')

src/finite-group-theory/transpositions.lagda.md

@@ -263,19 +263,19 @@ module _
       is-not-identity-swap-2-Element-Type
         ( 2-element-type-2-Element-Decidable-Subtype P)
         ( eq-htpy-equiv
-          ( λ { (pair x p) →
-                eq-pair-Σ
-                  ( ( ap
-                      ( map-transposition' P x)
-                      ( eq-is-prop
-                        ( is-prop-is-decidable
-                          ( is-prop-is-in-2-Element-Decidable-Subtype P x))
-                          { y =
-                            is-decidable-subtype-subtype-2-Element-Decidable-Subtype
-                              ( P)
-                              ( x)})) ∙
-                    ( htpy-eq f x))
-                  ( eq-is-in-2-Element-Decidable-Subtype P)}))
+          ( λ (x , p) →
+            eq-pair-Σ
+              ( ( ap
+                  ( map-transposition' P x)
+                  ( eq-is-prop
+                    ( is-prop-is-decidable
+                      ( is-prop-is-in-2-Element-Decidable-Subtype P x))
+                      { y =
+                        is-decidable-subtype-subtype-2-Element-Decidable-Subtype
+                          ( P)
+                          ( x)})) ∙
+                ( htpy-eq f x))
+              ( eq-is-in-2-Element-Decidable-Subtype P)))
 ```
 
 ### Any transposition on a type equipped with a counting is a standard transposition

src/foundation-core/equivalences.lagda.md

@@ -581,7 +581,7 @@ module _
                   ( inv (coherence-map-inv-is-equiv H x))
                   ( inv (ap-id p))) ∙
                 ( nat-htpy (is-section-map-inv-is-equiv H) p))))))
-      ( λ {refl → left-inv (is-retraction-map-inv-is-equiv H x)})
+      ( λ where refl → left-inv (is-retraction-map-inv-is-equiv H x))
 
   equiv-ap :
     (e : A ≃ B) (x y : A) → (x ＝ y) ≃ (map-equiv e x ＝ map-equiv e y)

src/foundation/0-connected-types.lagda.md

@@ -103,7 +103,7 @@ is-surjective-point-is-0-connected a H x =
   apply-universal-property-trunc-Prop
     ( mere-eq-is-0-connected H a x)
     ( trunc-Prop (fiber (point a) x))
-    ( λ {refl → unit-trunc-Prop (pair star refl)})
+    ( λ where refl → unit-trunc-Prop (star , refl))
 
 is-trunc-map-ev-point-is-connected :
   {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (a : A) →
@@ -117,7 +117,7 @@ is-trunc-map-ev-point-is-connected k {A} {B} a H K =
       ( universal-property-contr-is-contr star is-contr-unit B))
     ( is-trunc-map-precomp-Π-is-surjective k
       ( is-surjective-point-is-0-connected a H)
-      ( λ _ → pair B K))
+      ( λ _ → (B , K)))
 
 equiv-dependent-universal-property-is-0-connected :
   {l1 : Level} {A : UU l1} (a : A) → is-0-connected A →
@@ -140,11 +140,11 @@ abstract
   is-surjective-fiber-inclusion :
     {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
     is-0-connected A → (a : A) → is-surjective (fiber-inclusion B a)
-  is-surjective-fiber-inclusion {B = B} C a (pair x b) =
+  is-surjective-fiber-inclusion {B = B} C a (x , b) =
     apply-universal-property-trunc-Prop
       ( mere-eq-is-0-connected C a x)
-      ( trunc-Prop (fiber (fiber-inclusion B a) (pair x b)))
-      ( λ { refl → unit-trunc-Prop (pair b refl)})
+      ( trunc-Prop (fiber (fiber-inclusion B a) (x , b)))
+      ( λ where refl → unit-trunc-Prop (b , refl))
 
 abstract
   mere-eq-is-surjective-fiber-inclusion :
@@ -153,7 +153,7 @@ abstract
     (x : A) → mere-eq a x
   mere-eq-is-surjective-fiber-inclusion a H x =
     apply-universal-property-trunc-Prop
-      ( H (λ x → unit) (pair x star))
+      ( H (λ x → unit) (x , star))
       ( mere-eq-Prop a x)
       ( λ u → unit-trunc-Prop (ap pr1 (pr2 u)))
 

src/foundation/apartness-relations.lagda.md

@@ -199,16 +199,17 @@ module _
           ( disj-Prop
             ( rel-apart-function-into-Type-With-Apartness X Y f h)
             ( rel-apart-function-into-Type-With-Apartness X Y g h))
-          ( λ { (inl b) →
-                inl-disj-Prop
-                  ( rel-apart-function-into-Type-With-Apartness X Y f h)
-                  ( rel-apart-function-into-Type-With-Apartness X Y g h)
-                  ( unit-trunc-Prop (x , b)) ;
-                (inr b) →
-                inr-disj-Prop
-                  ( rel-apart-function-into-Type-With-Apartness X Y f h)
-                  ( rel-apart-function-into-Type-With-Apartness X Y g h)
-                  ( unit-trunc-Prop (x , b))}))
+          ( λ where
+            ( inl b) →
+              inl-disj-Prop
+                ( rel-apart-function-into-Type-With-Apartness X Y f h)
+                ( rel-apart-function-into-Type-With-Apartness X Y g h)
+                ( unit-trunc-Prop (x , b))
+            ( inr b) →
+              inr-disj-Prop
+                ( rel-apart-function-into-Type-With-Apartness X Y f h)
+                ( rel-apart-function-into-Type-With-Apartness X Y g h)
+                ( unit-trunc-Prop (x , b))))
 
   exp-Type-With-Apartness : Type-With-Apartness (l1 ⊔ l2) (l1 ⊔ l3)
   pr1 exp-Type-With-Apartness = X → type-Type-With-Apartness Y

src/foundation/connected-types.lagda.md

@@ -106,6 +106,6 @@ module _
                   ( trunc (succ-𝕋 k) A)
                   ( unit-trunc a)
                   ( unit-trunc x))
-                ( λ { refl → refl})
+                ( λ where refl → refl)
                 ( center (K a x)))))
 ```

src/foundation/embeddings.lagda.md

@@ -277,9 +277,10 @@ module _
     is-emb-equiv-refl-to-refl e p x y =
       is-equiv-htpy-equiv
         (inv-equiv (e x y))
-        λ { refl →
-              inv (is-retraction-map-inv-equiv (e x x) refl) ∙
-              ap (map-equiv (inv-equiv (e x x))) (p x)}
+        ( λ where
+          refl →
+            inv (is-retraction-map-inv-equiv (e x x) refl) ∙
+            ap (map-equiv (inv-equiv (e x x))) (p x))
 ```
 
 ### Embeddings are closed under pullback