formatting

src/elementary-number-theory/2-adic-decomposition.lagda.md

@@ -41,15 +41,24 @@ open import foundation-core.injective-maps
 
 ## Idea
 
-The {{#concept "2-adic decomposition" Agda=2-adic-decomposition-ℕ}} of a [natural number](elementary-number-theory.natural-numbers.md) $n$ is a factorization of $n$ into a [power](elementary-number-theory.exponentiation-natural-numbers.md) of $2$ and an [odd](elementary-number-theory.parity-natural-numbers.md) natural number.
+The {{#concept "2-adic decomposition" Agda=2-adic-decomposition-ℕ}} of a
+[natural number](elementary-number-theory.natural-numbers.md) $n$ is a
+factorization of $n$ into a
+[power](elementary-number-theory.exponentiation-natural-numbers.md) of $2$ and
+an [odd](elementary-number-theory.parity-natural-numbers.md) natural number.
 
-The $2$-adic decomposition of the natural numbers can be used to construct an [equivalence](foundation-core.equivalences.md) $\mathbb{N}\times\mathbb{N} \simeq \mathbb{N}$ by mapping
+The $2$-adic decomposition of the natural numbers can be used to construct an
+[equivalence](foundation-core.equivalences.md)
+$\mathbb{N}\times\mathbb{N} \simeq \mathbb{N}$ by mapping
 
 $$
   (m , n) \mapsto 2^m(2n + 1) - 1.
 $$
 
-The exponent $k$ such that the 2-adic decomposition of $n$ is $2^k \cdot m=n$ is called the {{#concept "2-adic valuation" Disambiguation="natural numbers" Agda=valuation-2-adic-decomposition-ℕ}} of $n$.
+The exponent $k$ such that the 2-adic decomposition of $n$ is $2^k \cdot m=n$ is
+called the
+{{#concept "2-adic valuation" Disambiguation="natural numbers" Agda=valuation-2-adic-decomposition-ℕ}}
+of $n$.
 
 ## Definitions
 
@@ -132,12 +141,12 @@ pr2 (pr2 (2-adic-decomposition-is-odd-ℕ n H)) =
 module _
   (n : ℕ) (H : 1 ≤-ℕ n)
   where
-  
+
   valuation-2-adic-decomposition-nat-ℕ :
     ℕ
   valuation-2-adic-decomposition-nat-ℕ =
     valuation-largest-power-divisor-ℕ 2 n star H
-  
+
   div-exp-valuation-2-adic-decomposition-nat-ℕ :
     div-ℕ (2 ^ℕ valuation-2-adic-decomposition-nat-ℕ) n
   div-exp-valuation-2-adic-decomposition-nat-ℕ =

src/elementary-number-theory/addition-natural-numbers.lagda.md

@@ -28,9 +28,15 @@ open import foundation.sets
 
 ## Idea
 
-The {{#concept "addition" Disambiguation="natural numbers" Agda=_+ℕ_}} operation on the [natural numbers](elementary-number-theory.natural-numbers.md) is a binary operation $m,n\mapsto m+n$ on the natural numbers given by $n$ times iteratively taking the successor of the number $m$.
-
-The notation $+$ for addition and $-$ for subtraction appeared first in print in 1489 in _Behende und hüpsche Rechenung auff allen Kauffmanschafft_ by [Johannes Widmann](https://en.wikipedia.org/wiki/Johannes_Widmann), for example on page 327 of {{#cite Widmann1489}}.
+The {{#concept "addition" Disambiguation="natural numbers" Agda=_+ℕ_}} operation
+on the [natural numbers](elementary-number-theory.natural-numbers.md) is a
+binary operation $m,n\mapsto m+n$ on the natural numbers given by $n$ times
+iteratively taking the successor of the number $m$.
+
+The notation $+$ for addition and $-$ for subtraction appeared first in print in
+1489 in _Behende und hüpsche Rechenung auff allen Kauffmanschafft_ by
+[Johannes Widmann](https://en.wikipedia.org/wiki/Johannes_Widmann), for example
+on page 327 of {{#cite Widmann1489}}.
 
 ## Definitions
 

src/elementary-number-theory/bounded-divisibility-natural-numbers.lagda.md

@@ -34,9 +34,25 @@ open import foundation.universe-levels
 
 ## Idea
 
-Consider two [natural numbers](elementary-number-theory.natural-numbers.md) `m` and `n`. The {{#concept "bounded divisibility relation" Disambiguation="natural numbers" Agda=bounded-div-ℕ}} is a [binary relation](foundation.binary-relations.md) on the type of [natural numbers](elementary-number-theory.natural-numbers.md), where we say that a number `n` is bounded divisible by `m` if there is an integer `q ≤ n` such that `q * m ＝ n`.
-
-The bounded divisibility relation is a slight strengthening of the [divisibility relation](elementary-number-theory.divisibility-natural-numbers.md) by ensuring that the quotient is bounded from above by `n`. This ensures that the bounded divisibility relation is valued in [propositions](foundation-core.propositions.md) for all `m` and `n`, unlike the divisibility relation. Since the bounded divisibility relation is [logically equivalent](foundation.logical-equivalences.md) to the divisibility relation, but it is always valued in the propositions, we use the bounded divisibility relation in the definition of the [poset](order-theory.posets.md) of the [natural numbers ordered by division](elementary-number-theory.poset-of-natural-numbers-ordered-by-divisibility.md).
+Consider two [natural numbers](elementary-number-theory.natural-numbers.md) `m`
+and `n`. The
+{{#concept "bounded divisibility relation" Disambiguation="natural numbers" Agda=bounded-div-ℕ}}
+is a [binary relation](foundation.binary-relations.md) on the type of
+[natural numbers](elementary-number-theory.natural-numbers.md), where we say
+that a number `n` is bounded divisible by `m` if there is an integer `q ≤ n`
+such that `q * m ＝ n`.
+
+The bounded divisibility relation is a slight strengthening of the
+[divisibility relation](elementary-number-theory.divisibility-natural-numbers.md)
+by ensuring that the quotient is bounded from above by `n`. This ensures that
+the bounded divisibility relation is valued in
+[propositions](foundation-core.propositions.md) for all `m` and `n`, unlike the
+divisibility relation. Since the bounded divisibility relation is
+[logically equivalent](foundation.logical-equivalences.md) to the divisibility
+relation, but it is always valued in the propositions, we use the bounded
+divisibility relation in the definition of the [poset](order-theory.posets.md)
+of the
+[natural numbers ordered by division](elementary-number-theory.poset-of-natural-numbers-ordered-by-divisibility.md).
 
 ## Definitions
 
@@ -81,7 +97,9 @@ is-nonzero-quotient-bounded-div-ℕ m n N H refl =
 
 ### If a nonzero number `n` is bounded divisible by `m`, then `m` is bounded from above by `n`
 
-**Proof.** Suppose that `q ≤ n` is such that `q * m ＝ n`. Since `n` is assumed to be nonzero, it follows that `q` is nonzero. Therefore it follows that `m ≤ q * m = n`.
+**Proof.** Suppose that `q ≤ n` is such that `q * m ＝ n`. Since `n` is assumed
+to be nonzero, it follows that `q` is nonzero. Therefore it follows that
+`m ≤ q * m = n`.
 
 ```agda
 upper-bound-divisor-bounded-div-ℕ :
@@ -140,7 +158,8 @@ concatenate-eq-bounded-div-eq-ℕ refl p refl = p
 
 ### The quotients of a natural number `n` by two natural numbers `c` and `d` are equal if `c` and `d` are equal
 
-Since the quotient is defined in terms of explicit proofs of divisibility, we assume arbitrary proofs of dibisibility on both sides.
+Since the quotient is defined in terms of explicit proofs of divisibility, we
+assume arbitrary proofs of dibisibility on both sides.
 
 ```agda
 eq-quotient-bounded-div-eq-divisor-ℕ :
@@ -160,7 +179,9 @@ eq-quotient-bounded-div-eq-divisor-ℕ c d n N p H I =
 
 ### If two natural numbers are equal and one is divisible by a number `d`, then the other is divisible by `d` and their quotients are the same
 
-The first part of the claim was proven above. Since the quotient is defined in terms of explicit proofs of divisibility, we assume arbitrary proofs of dibisibility on both sides.
+The first part of the claim was proven above. Since the quotient is defined in
+terms of explicit proofs of divisibility, we assume arbitrary proofs of
+dibisibility on both sides.
 
 ```agda
 eq-quotient-bounded-div-eq-is-nonzero-divisor-ℕ :
@@ -366,7 +387,7 @@ upper-bound-quotient-transitive-bounded-div-ℕ (succ-ℕ m) n k K H =
     ( k)
     ( is-nonzero-succ-ℕ m)
     ( eq-quotient-transitive-bounded-div-ℕ (succ-ℕ m) n k K H)
-  
+
 transitive-bounded-div-ℕ : is-transitive bounded-div-ℕ
 pr1 (transitive-bounded-div-ℕ m n k K H) =
   quotient-transitive-bounded-div-ℕ m n k K H

src/elementary-number-theory/bounded-natural-numbers.lagda.md

@@ -31,13 +31,16 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-The type of {{#concept "bounded natural numbers" Agda=bounded-ℕ}} with upper bound $n$ is the type
+The type of {{#concept "bounded natural numbers" Agda=bounded-ℕ}} with upper
+bound $n$ is the type
 
 $$
   \mathbb{N}_{\leq n} := \{k : ℕ \mid k \leq n\}.
 $$
 
-The type $\mathbb{N}_{\leq n}$ is [equivalent](foundation-core.equivalences.md) to the [standard finite type](univalent-combinatorics.standard-finite-types.md) $\mathsf{Fin}(n+1)$.
+The type $\mathbb{N}_{\leq n}$ is [equivalent](foundation-core.equivalences.md)
+to the [standard finite type](univalent-combinatorics.standard-finite-types.md)
+$\mathsf{Fin}(n+1)$.
 
 ## Definition
 

src/elementary-number-theory/congruence-natural-numbers.lagda.md

@@ -29,15 +29,30 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-Two [natural numbers](elementary-number-theory.natural-numbers.md) `x` and `y` are said to be {{#concept "congruent" Disambiguation="natural numbers" Agda=cong-ℕ WDID=Q3773677 WD="congruence of integers"}} modulo `k` if their [distance](elementary-number-theory.distance-natural-numbers.md) `dist-ℕ x y` is [divisible](elementary-number-theory.divisibility-natural-numbers.md) by `k`, i.e., if
+Two [natural numbers](elementary-number-theory.natural-numbers.md) `x` and `y`
+are said to be
+{{#concept "congruent" Disambiguation="natural numbers" Agda=cong-ℕ WDID=Q3773677 WD="congruence of integers"}}
+modulo `k` if their
+[distance](elementary-number-theory.distance-natural-numbers.md) `dist-ℕ x y` is
+[divisible](elementary-number-theory.divisibility-natural-numbers.md) by `k`,
+i.e., if
 
 ```text
   k | dist-ℕ x y.
 ```
 
-For each natural number `k`, the congruence relation modulo `k` defines an [equivalence relation](foundation.equivalence-relations.md). Furthermore, the congruence relations respect [addition](elementary-number-theory.addition-natural-numbers.md) and [multiplication](elementary-number-theory.multiplication-natural-numbers.md).
-
-[Quotienting](foundation.set-quotients.md) by the congruence relation leads to [modular arithmetic](elementary-number-theory.modular-arithmetic.md). Properties of the congruence relation with respect to the [standard finite types](univalent-combinatorics.standard-finite-types.md) are formalized in the file [`modular-arithmetic-standard-finite-types`](elementary-number-theory.modular-arithmetic-standard-finite-types.md).
+For each natural number `k`, the congruence relation modulo `k` defines an
+[equivalence relation](foundation.equivalence-relations.md). Furthermore, the
+congruence relations respect
+[addition](elementary-number-theory.addition-natural-numbers.md) and
+[multiplication](elementary-number-theory.multiplication-natural-numbers.md).
+
+[Quotienting](foundation.set-quotients.md) by the congruence relation leads to
+[modular arithmetic](elementary-number-theory.modular-arithmetic.md). Properties
+of the congruence relation with respect to the
+[standard finite types](univalent-combinatorics.standard-finite-types.md) are
+formalized in the file
+[`modular-arithmetic-standard-finite-types`](elementary-number-theory.modular-arithmetic-standard-finite-types.md).
 
 ## Properties
 

src/elementary-number-theory/decidable-maps-natural-numbers.lagda.md

@@ -14,4 +14,9 @@ module elementary-number-theory.decidable-maps-natural-numbers where
 
 ## Idea
 
-Consider a map $f : A \to \mathbb{N}$ into the [natural numbers](elementary-number-theory.natural-numbers.md). Then $f$ is said to be a {{#concept "decidable map" Disambiguation="natural numbers"}} if its [fibers](foundation-core.fibers-of-maps.md) are [decidable](foundation.decidable-types.md), i.e., if it is a [decidable map](foundation.decidable-maps.md).
+Consider a map $f : A \to \mathbb{N}$ into the
+[natural numbers](elementary-number-theory.natural-numbers.md). Then $f$ is said
+to be a {{#concept "decidable map" Disambiguation="natural numbers"}} if its
+[fibers](foundation-core.fibers-of-maps.md) are
+[decidable](foundation.decidable-types.md), i.e., if it is a
+[decidable map](foundation.decidable-maps.md).

src/elementary-number-theory/decidable-subtypes-natural-numbers.lagda.md

@@ -39,9 +39,18 @@ open import univalent-combinatorics.decidable-subtypes
 
 ## Idea
 
-In this file we study [decidable subtypes](foundation.decidable-subtypes.md) of the [natural numbers](elementary-number-theory.natural-numbers.md). The type of all decidable subtypes of the natural numbers is the *decidable powerset of the natural numbers*.
-
-As a direct consequence of the [well-ordering principle](elementary-number-theory.well-ordering-principle-natural-numbers.md) of the natural numbers, which is formulated for decidable structures over the natural numbers, it follows that every [inhabited](foundation.inhabited-subtypes.md) decidable subtype of the natural numbers has a least element. We also show that every finite decidable subtype has a largest element.
+In this file we study [decidable subtypes](foundation.decidable-subtypes.md) of
+the [natural numbers](elementary-number-theory.natural-numbers.md). The type of
+all decidable subtypes of the natural numbers is the _decidable powerset of the
+natural numbers_.
+
+As a direct consequence of the
+[well-ordering principle](elementary-number-theory.well-ordering-principle-natural-numbers.md)
+of the natural numbers, which is formulated for decidable structures over the
+natural numbers, it follows that every
+[inhabited](foundation.inhabited-subtypes.md) decidable subtype of the natural
+numbers has a least element. We also show that every finite decidable subtype
+has a largest element.
 
 ## Properties
 
@@ -155,4 +164,3 @@ module _
         ( P ∘ pr1)
         ( is-finite-bounded-ℕ m))
 ```
-

src/elementary-number-theory/distance-natural-numbers.lagda.md

@@ -31,10 +31,17 @@ open import foundation.universe-levels
 The
 {{#concept "distance function" Disambiguation="natural numbers" Agda=dist-ℕ}}
 between [natural numbers](elementary-number-theory.natural-numbers.md) measures
-how far two natural numbers are apart. If the [inequality](elementary-number-theory.inequality-natural-numbers.md) $x \leq y$ holds, then the distance between $x$ and $y$ is the unique natural number $d$ equipped with an [identification](foundation-core.identity-types.md) $x + d = y$.
-
-**Note.** In the agda-unimath library, we often
-prefer to work with `dist-ℕ` over the subtraction operation, which is either partially defined or it returns nonsensical values. Not only is the distance function sensibly defined for any pair of natural numbers, but it also satisfies the more pleasant and predictable properties of a [metric](metric-spaces.metric-spaces.md).
+how far two natural numbers are apart. If the
+[inequality](elementary-number-theory.inequality-natural-numbers.md) $x \leq y$
+holds, then the distance between $x$ and $y$ is the unique natural number $d$
+equipped with an [identification](foundation-core.identity-types.md)
+$x + d = y$.
+
+**Note.** In the agda-unimath library, we often prefer to work with `dist-ℕ`
+over the subtraction operation, which is either partially defined or it returns
+nonsensical values. Not only is the distance function sensibly defined for any
+pair of natural numbers, but it also satisfies the more pleasant and predictable
+properties of a [metric](metric-spaces.metric-spaces.md).
 
 ## Definition
 

src/elementary-number-theory/divisibility-natural-numbers.lagda.md

@@ -67,7 +67,8 @@ then the type `div-ℕ m n` is always a
 The divisibility relation is
 [logically equivalent](foundation.logical-equivalences.md), though not
 [equivalent](foundation-core.equivalences.md), to the
-[bounded divisibility relation](elementary-number-theory.bounded-divisibility-natural-numbers.md), which is defined by
+[bounded divisibility relation](elementary-number-theory.bounded-divisibility-natural-numbers.md),
+which is defined by
 
 ```text
   bounded-div-ℕ m n := Σ (k : ℕ), (k ≤ n) × (k *ℕ m ＝ n).
@@ -78,15 +79,24 @@ The discrepancy between divisibility and bounded divisibility is manifested at
 [contractible](foundation-core.contractible-types.md). For all other values we
 have `div-ℕ m n ≃ bounded-div-ℕ m n`.
 
-When a natural number `n is divisible by a natural number `m`, with an element `H : div-ℕ m n`, then we define the {{#concept "quotient" Disambiguation="divisibility of natural numbers" Agda=quotient-div-ℕ}} to be the unique number `q ≤ n` such that `q * m ＝ n`. 
+When a natural number
+`n is divisible by a natural number `m`, with an element `H : div-ℕ m
+n`, then we define the {{#concept "quotient" Disambiguation="divisibility of natural numbers" Agda=quotient-div-ℕ}} to be the unique number `q
+≤ n`such that`q \* m ＝ n`.
 
 ## Definitions
 
 ### The divisibility relation on the natural numbers
 
-We introduce the divisibility relation on the natural numbers, and some infrastructure.
+We introduce the divisibility relation on the natural numbers, and some
+infrastructure.
 
-**Note:** Perhaps a more natural name for `pr1-div-ℕ`, the number `q` such that `q * d ＝ n`, would be `quotient-div-ℕ`. However, since the divisibility relation is not always a proposition, the quotient could have some undesirable properties. Later in this file, we will define `quotient-div-ℕ` to the the quotient of the bounded divisibility relation, which is logically equivalent to the divisibility relation.
+**Note:** Perhaps a more natural name for `pr1-div-ℕ`, the number `q` such that
+`q * d ＝ n`, would be `quotient-div-ℕ`. However, since the divisibility
+relation is not always a proposition, the quotient could have some undesirable
+properties. Later in this file, we will define `quotient-div-ℕ` to the the
+quotient of the bounded divisibility relation, which is logically equivalent to
+the divisibility relation.
 
 ```agda
 module _
@@ -245,7 +255,8 @@ concatenate-eq-div-eq-ℕ refl p refl = p
 
 ### The quotients of a natural number `n` by two natural numbers `c` and `d` are equal if `c` and `d` are equal
 
-Since the quotient is defined in terms of explicit proofs of divisibility, we assume arbitrary proofs of dibisibility on both sides.
+Since the quotient is defined in terms of explicit proofs of divisibility, we
+assume arbitrary proofs of dibisibility on both sides.
 
 ```agda
 eq-quotient-div-eq-divisor-ℕ :
@@ -265,7 +276,9 @@ eq-quotient-div-eq-divisor-ℕ c d n N p H I =
 
 ### If two natural numbers are equal and one is divisible by a number `d`, then the other is divisible by `d` and their quotients are the same
 
-The first part of the claim was proven above. Since the quotient is defined in terms of explicit proofs of divisibility, we assume arbitrary proofs of dibisibility on both sides.
+The first part of the claim was proven above. Since the quotient is defined in
+terms of explicit proofs of divisibility, we assume arbitrary proofs of
+dibisibility on both sides.
 
 ```agda
 eq-quotient-div-eq-is-nonzero-divisor-ℕ :