chore: fix some typos in the library (#1083)

### Note
"Non-" is commonly spelled without a hyphen in American English.
- https://www.oxfordlearnersdictionaries.com/definition/english/non
- https://en.wiktionary.org/wiki/non-#Usage_notes

MIXFIX-OPERATORS.md

@@ -125,7 +125,7 @@ Below, we outline a list of general rules when assigning associativities.
   [function composition `_∘_`](foundation-core.function-types.md), can be
   assigned _any associativity_.
 
-- **Non-parametric arithmetic operators** are often naturally computed from left
+- **Nonparametric arithmetic operators** are often naturally computed from left
   to right. For instance, the expression `1 - 2 - 3` is computed as
   `(1 - 2) - 3 = -1 - 3 = -4`, hence should be _left associative_. This applies
   to addition, subtraction, multiplication, and division. Note that for

src/foundation/injective-maps.lagda.md

@@ -30,7 +30,7 @@ maps between general types it is recommended to use the notion of
 
 ## Definitions
 
-### Non-injective maps
+### Noninjective maps
 
 ```agda
 module _

src/foundation/noncontractible-types.lagda.md

@@ -1,4 +1,4 @@
-# Non-contractible types
+# Noncontractible types
 
 ```agda
 module foundation.noncontractible-types where

src/linear-algebra/functoriality-matrices.lagda.md

@@ -1,4 +1,4 @@
-# Functoriality of matrices
+# Functoriality of the type of matrices
 
 ```agda
 module linear-algebra.functoriality-matrices where
@@ -19,7 +19,7 @@ open import linear-algebra.matrices
 
 ## Idea
 
-An map `f : A → B` induces a map `matrix A m n → matrix B m n`.
+Any map `f : A → B` induces a map `matrix A m n → matrix B m n`.
 
 ## Definition
 

src/linear-algebra/functoriality-vectors.lagda.md

@@ -28,7 +28,7 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-Any map `f : A → B` determines a map `vec n A → vec n B` for every `n`.
+Any map `f : A → B` determines a map `vec A n → vec B n` for every `n`.
 
 ## Definition
 

src/linear-algebra/vectors-on-commutative-rings.lagda.md

@@ -27,7 +27,7 @@ open import linear-algebra.vectors-on-rings
 ## Idea
 
 Vectors on a commutative ring `R` are vectors on the underlying type of `R`. The
-commutative ring structur on `R` induces further structure on the type of
+commutative ring structure on `R` induces further structure on the type of
 vectors on `R`.
 
 ## Definitions

src/linear-algebra/vectors-on-commutative-semirings.lagda.md

@@ -27,7 +27,7 @@ open import linear-algebra.vectors-on-semirings
 ## Idea
 
 Vectors on a commutative semiring `R` are vectors on the underlying type of `R`.
-The commutative semiring structur on `R` induces further structure on the type
+The commutative semiring structure on `R` induces further structure on the type
 of vectors on `R`.
 
 ## Definitions

src/ring-theory/algebras-rings.lagda.md

@@ -34,7 +34,7 @@ An **algebra** over a [ring](ring-theory.rings.md) `R` consists of an
 
 ## Definitions
 
-### Non-unital algebras over a ring
+### Nonunital algebras over a ring
 
 ```agda
 has-bilinear-mul-left-module-Ring :

src/structured-types/noncoherent-h-spaces.lagda.md

@@ -1,4 +1,4 @@
-# Non-coherent H-spaces
+# Noncoherent H-spaces
 
 ```agda
 module structured-types.noncoherent-h-spaces where
@@ -43,7 +43,7 @@ unital-mul-Pointed-Type A =
     ( unit-laws-mul-Pointed-Type A)
 ```
 
-### Non-coherent Noncoherent-H-Spaces
+### Noncoherent H-Spaces
 
 ```agda
 noncoherent-h-space-structure :