chore: Replace strange whitespace (#1215)

A simple addition to our markdown conventions that replaces nonstandard
Unicode whitespace characters with normal spaces.

scripts/markdown_conventions.py

@@ -106,6 +106,10 @@ def find_ill_formed_block(mdcode):
         output = re.sub(
             r'(^|\n)(#+\s.*)[\.,:;!?¡¿]\s*($|\n)', r'\1\2\3', output)
 
+        # Replace strange whitespace with normal spaces
+        output = re.sub(
+            r'(?<!^)(?![ \t\r\n\f\v])\s', r' ', output)
+
         if output != inputText:
             with open(fpath, 'w') as f:
                 f.write(output)

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

@@ -615,33 +615,33 @@ is-least-element-head-list-fundamental-theorem-arithmetic-succ-ℕ :
     ( ℕ-Decidable-Total-Order)
     ( nat-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
     ( list-fundamental-theorem-arithmetic-ℕ
-      ( quotient-div-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
+      ( quotient-div-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
       ( leq-one-quotient-div-ℕ
         ( nat-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
         ( succ-ℕ x)
-        ( div-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
+        ( div-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
         ( preserves-leq-succ-ℕ 1 x H)))
 is-least-element-head-list-fundamental-theorem-arithmetic-succ-ℕ x H =
   is-least-element-list-least-prime-divisor-ℕ
     ( x)
     ( H)
     ( list-fundamental-theorem-arithmetic-ℕ
-      ( quotient-div-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
+      ( quotient-div-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
       ( leq-one-quotient-div-ℕ
         ( nat-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
         ( succ-ℕ x)
-        ( div-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
+        ( div-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
         ( preserves-leq-succ-ℕ 1 x H)))
     ( is-list-of-nontrivial-divisors-fundamental-theorem-arithmetic-ℕ
-      ( quotient-div-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
+      ( quotient-div-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
       ( leq-one-quotient-div-ℕ
         ( nat-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
         ( succ-ℕ x)
-        ( div-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
+        ( div-least-prime-divisor-ℕ (succ-ℕ x) (le-succ-leq-ℕ 1 x H))
         ( preserves-leq-succ-ℕ 1 x H)))
 
 is-sorted-least-element-list-fundamental-theorem-arithmetic-ℕ :
-  (x : ℕ) → (H : leq-ℕ 1 x) →
+  (x : ℕ) → (H : leq-ℕ 1 x) →
   is-sorted-least-element-list
     ( ℕ-Decidable-Total-Order)
     ( list-fundamental-theorem-arithmetic-ℕ x H)

src/elementary-number-theory/prime-numbers.lagda.md

@@ -121,7 +121,7 @@ le-one-is-prime-ℕ (succ-ℕ (succ-ℕ n)) x = star
 
 ```agda
 is-prop-is-prime-ℕ :
-  (n : ℕ) → is-prop (is-prime-ℕ n)
+  (n : ℕ) → is-prop (is-prime-ℕ n)
 is-prop-is-prime-ℕ n =
   is-prop-Π
     ( λ x →

src/finite-algebra/commutative-finite-rings.lagda.md

@@ -624,6 +624,6 @@ module _
           ( is-finite-type-𝔽 X)
           ( λ _ →
             is-finite-Π
-              ( is-finite-type-𝔽 X)
+              ( is-finite-type-𝔽 X)
               ( λ _ → is-finite-eq-𝔽 X)))
 ```

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

@@ -469,7 +469,7 @@ htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin :
 htpy-conjugate-transposition-swap-two-last-elements-transposition-Fin n x neq =
   ( ( htpy-whisker-conjugate
         ( map-transposition-Fin
-          ( succ-ℕ (succ-ℕ n))
+          ( succ-ℕ (succ-ℕ n))
           ( inl-Fin (succ-ℕ n) x)
           ( neg-two-Fin (succ-ℕ n))
           ( neq ∘ is-injective-inl-Fin (succ-ℕ n)))

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

@@ -471,7 +471,7 @@ module _
     element-two-elements-transposition ≠
     other-element-two-elements-transposition
   neq-elements-two-elements-transposition =
-    pr1 (pr2 (pr2 two-elements-transposition))
+    pr1 (pr2 (pr2 two-elements-transposition))
 
   abstract
     cases-eq-two-elements-transposition :
@@ -1239,7 +1239,7 @@ module _
     ( ( ap
         ( λ w →
           map-equiv
-            ( standard-transposition H npyz ∘e standard-transposition H npxy)
+            ( standard-transposition H npyz ∘e standard-transposition H npxy)
             ( w))
         ( is-fixed-point-standard-transposition
           ( H)

src/foundation/coproduct-decompositions-subuniverse.lagda.md

@@ -104,7 +104,7 @@ module _
 
   right-iterated-binary-coproduct-Decomposition-subuniverse : UU (lsuc l1 ⊔ l2)
   right-iterated-binary-coproduct-Decomposition-subuniverse =
-    Σ ( binary-coproduct-Decomposition-subuniverse P X)
+    Σ ( binary-coproduct-Decomposition-subuniverse P X)
       ( λ d →
         binary-coproduct-Decomposition-subuniverse P
           ( right-summand-binary-coproduct-Decomposition-subuniverse P X d))
@@ -242,12 +242,12 @@ module _
     is-torsorial-Eq-structure
       ( is-torsorial-equiv-subuniverse P
         ( left-summand-binary-coproduct-Decomposition-subuniverse P A X))
-      ( left-summand-binary-coproduct-Decomposition-subuniverse P A X ,
+      ( left-summand-binary-coproduct-Decomposition-subuniverse P A X ,
         id-equiv)
       ( is-torsorial-Eq-structure
         ( is-torsorial-equiv-subuniverse P
-          ( right-summand-binary-coproduct-Decomposition-subuniverse P A X))
-        ( right-summand-binary-coproduct-Decomposition-subuniverse P A X ,
+          ( right-summand-binary-coproduct-Decomposition-subuniverse P A X))
+        ( right-summand-binary-coproduct-Decomposition-subuniverse P A X ,
           id-equiv)
         ( is-torsorial-htpy-equiv
           ( equiv-coproduct id-equiv id-equiv ∘e

src/foundation/coproduct-decompositions.lagda.md

@@ -302,7 +302,7 @@ module _
             ( pr1
               ( compute-left-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                 ( pr1 y)
-                ( inv (pr2 y))))) ∙
+                ( inv (pr2 y))))) ∙
           ap
             inl
             ( eq-pair-Σ
@@ -365,7 +365,7 @@ module _
             ( pr1
               ( compute-right-matching-correspondence-binary-coproduct-Decomposition-map-into-Fin-Two-ℕ
                 ( pr1 y)
-                ( inv (pr2 y))))) ∙
+                ( inv (pr2 y))))) ∙
           ap
             inr
             ( eq-pair-Σ

src/foundation/iterated-cartesian-product-types.lagda.md

@@ -145,7 +145,7 @@ equiv-product-iterated-product-lists (cons x p) q =
 ```agda
 permutation-iterated-product-Fin-Π :
   {l : Level} (n : ℕ) (A : (Fin n → UU l)) (t : Permutation n) → UU l
-permutation-iterated-product-Fin-Π n A t =
+permutation-iterated-product-Fin-Π n A t =
   iterated-product-Fin-Π n (A ∘ map-equiv t)
 
 equiv-permutation-iterated-product-Fin-Π :
@@ -162,7 +162,7 @@ eq-permutation-iterated-product-Fin-Π n A t =
 
 permutation-iterated-product-Fin-recursive :
   {l : Level} (n : ℕ) (A : (Fin n → UU l)) (t : Permutation n) → UU l
-permutation-iterated-product-Fin-recursive n A t =
+permutation-iterated-product-Fin-recursive n A t =
   iterated-product-Fin-recursive n (A ∘ map-equiv t)
 
 equiv-permutation-iterated-product-Fin-recursive :

src/lists/functoriality-lists.lagda.md

@@ -61,7 +61,7 @@ length-map-list f (cons x l) =
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
   (f : A → B)
   where
 

src/lists/permutation-lists.lagda.md

@@ -173,7 +173,7 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2}
   (b : B)
   (μ : A → (B → B))
-  (C : commutative-fold-vec μ)
+  (C : commutative-fold-vec μ)
   where
 
   invariant-fold-vec-tr :

src/lists/permutation-vectors.lagda.md

@@ -222,7 +222,7 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2}
   (b : B)
   (μ : A → (B → B))
-  (C : commutative-fold-vec μ)
+  (C : commutative-fold-vec μ)
   where
 
   invariant-swap-two-last-elements-transposition-fold-vec :

src/lists/quicksort-lists.lagda.md

@@ -92,7 +92,7 @@ module _
       refl-leq-ℕ (length-list (cons y l))
 
     inequality-length-quicksort-list-divide-leq :
-      (x : type-Decidable-Total-Order X) →
+      (x : type-Decidable-Total-Order X) →
       (l : list (type-Decidable-Total-Order X)) →
       length-list (quicksort-list-divide-leq x l) ≤-ℕ length-list l
     inequality-length-quicksort-list-divide-leq x nil = star
@@ -129,7 +129,7 @@ module _
       succ-leq-ℕ (length-list l)
 
     inequality-length-quicksort-list-divide-strict-greater :
-      (x : type-Decidable-Total-Order X) →
+      (x : type-Decidable-Total-Order X) →
       (l : list (type-Decidable-Total-Order X)) →
       length-list (quicksort-list-divide-strict-greater x l) ≤-ℕ length-list l
     inequality-length-quicksort-list-divide-strict-greater x nil = star

src/lists/sort-by-insertion-vectors.lagda.md

@@ -206,7 +206,7 @@ module _
 
   eq-permute-vec-permutation-insertion-sort-vec :
     {n : ℕ}
-    (v : vec (type-Decidable-Total-Order X) n) →
+    (v : vec (type-Decidable-Total-Order X) n) →
     insertion-sort-vec v ＝ permute-vec n v (permutation-insertion-sort-vec v)
   eq-permute-vec-permutation-insertion-sort-vec {0} empty-vec = refl
   eq-permute-vec-permutation-insertion-sort-vec {1} (x ∷ empty-vec) = refl
@@ -308,12 +308,12 @@ module _
   is-sorting-insertion-sort-vec {succ-ℕ (succ-ℕ n)} (x ∷ y ∷ v) =
     helper-is-sorting-insertion-sort-vec
       ( x)
-      ( head-vec (insertion-sort-vec (y ∷ v)))
+      ( head-vec (insertion-sort-vec (y ∷ v)))
       ( tail-vec (insertion-sort-vec (y ∷ v)))
       ( is-leq-or-strict-greater-Decidable-Total-Order X _ _)
       ( tr
         ( λ l → is-sorted-vec X l)
-        ( inv (cons-head-tail-vec n (insertion-sort-vec (y ∷ v))))
+        ( inv (cons-head-tail-vec n (insertion-sort-vec (y ∷ v))))
         ( is-sorting-insertion-sort-vec (y ∷ v)))
 ```
 

src/order-theory/decidable-preorders.lagda.md

@@ -46,7 +46,7 @@ module _
   is-prop-is-decidable-leq-Preorder =
     is-prop-type-Prop is-decidable-leq-Preorder-Prop
 
-Decidable-Preorder : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Decidable-Preorder : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
 Decidable-Preorder l1 l2 = Σ (Preorder l1 l2) is-decidable-leq-Preorder
 
 module _

src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md

@@ -348,7 +348,7 @@ module _
             ( C1)
             ( C2)
             ( S)
-            ( cauchy-composition-unit-species-subuniverse P Q C4)
+            ( cauchy-composition-unit-species-subuniverse P Q C4)
             ( inclusion-subuniverse P X)) ∘e
           ( ( equiv-Σ-extension-species-subuniverse
               ( P)
@@ -431,7 +431,7 @@ module _
                   ( λ y →
                     cauchy-composition-species-types
                       ( Σ-extension-species-subuniverse
-                        ( P)
+                        ( P)
                         ( subuniverse-global-subuniverse Q l4)
                         ( T))
                       ( Σ-extension-species-subuniverse

src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md

@@ -49,7 +49,7 @@ module _
     UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l5)
   cauchy-series-species-subuniverse =
     Σ ( type-subuniverse P)
-      ( λ U → inclusion-subuniverse Q (S U) × (inclusion-subuniverse P U → X))
+      ( λ U → inclusion-subuniverse Q (S U) × (inclusion-subuniverse P U → X))
 ```
 
 ## Property