From 70f0e710d18fef3d4ebfb4049627209027ba33a3 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 19 Mar 2024 15:14:08 +0100 Subject: [PATCH] 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 | 2 +- src/foundation/injective-maps.lagda.md | 2 +- src/foundation/noncontractible-types.lagda.md | 2 +- src/linear-algebra/functoriality-matrices.lagda.md | 4 ++-- src/linear-algebra/functoriality-vectors.lagda.md | 2 +- src/linear-algebra/vectors-on-commutative-rings.lagda.md | 2 +- src/linear-algebra/vectors-on-commutative-semirings.lagda.md | 2 +- src/ring-theory/algebras-rings.lagda.md | 2 +- src/structured-types/noncoherent-h-spaces.lagda.md | 4 ++-- 9 files changed, 11 insertions(+), 11 deletions(-) diff --git a/MIXFIX-OPERATORS.md b/MIXFIX-OPERATORS.md index a953310e23..4ec18bd8cc 100644 --- a/MIXFIX-OPERATORS.md +++ b/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 diff --git a/src/foundation/injective-maps.lagda.md b/src/foundation/injective-maps.lagda.md index 8dc194c23a..5eaf79f193 100644 --- a/src/foundation/injective-maps.lagda.md +++ b/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 _ diff --git a/src/foundation/noncontractible-types.lagda.md b/src/foundation/noncontractible-types.lagda.md index e6260a2949..537377c85d 100644 --- a/src/foundation/noncontractible-types.lagda.md +++ b/src/foundation/noncontractible-types.lagda.md @@ -1,4 +1,4 @@ -# Non-contractible types +# Noncontractible types ```agda module foundation.noncontractible-types where diff --git a/src/linear-algebra/functoriality-matrices.lagda.md b/src/linear-algebra/functoriality-matrices.lagda.md index 6dc3086859..1c0b419bd0 100644 --- a/src/linear-algebra/functoriality-matrices.lagda.md +++ b/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 diff --git a/src/linear-algebra/functoriality-vectors.lagda.md b/src/linear-algebra/functoriality-vectors.lagda.md index 92dfaa93f4..61c74c2380 100644 --- a/src/linear-algebra/functoriality-vectors.lagda.md +++ b/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 diff --git a/src/linear-algebra/vectors-on-commutative-rings.lagda.md b/src/linear-algebra/vectors-on-commutative-rings.lagda.md index 8caf08c04e..83724fd171 100644 --- a/src/linear-algebra/vectors-on-commutative-rings.lagda.md +++ b/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 diff --git a/src/linear-algebra/vectors-on-commutative-semirings.lagda.md b/src/linear-algebra/vectors-on-commutative-semirings.lagda.md index 54d902a82b..37cfe9c5b2 100644 --- a/src/linear-algebra/vectors-on-commutative-semirings.lagda.md +++ b/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 diff --git a/src/ring-theory/algebras-rings.lagda.md b/src/ring-theory/algebras-rings.lagda.md index e4b2f3d1c9..ff618c84d6 100644 --- a/src/ring-theory/algebras-rings.lagda.md +++ b/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 : diff --git a/src/structured-types/noncoherent-h-spaces.lagda.md b/src/structured-types/noncoherent-h-spaces.lagda.md index 2ae47edd38..bf3ba3b5d1 100644 --- a/src/structured-types/noncoherent-h-spaces.lagda.md +++ b/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 :