Fixes typos identified in #2154

CHANGELOG.md

@@ -539,7 +539,7 @@ Non-backwards compatible changes
   3. Finally, if the above approaches are not viable then you may be forced to explicitly
      use `cong` combined with a lemma that proves the old reduction behaviour.
 
-* Similarly, in order to prevent reduction, the equality `_≃_` in `Data.Rational.Base` 
+* Similarly, in order to prevent reduction, the equality `_≃_` in `Data.Rational.Base`
   has been made into a data type with the single constructor `*≡*`. The destructor `drop-*≡*`
   has been added to `Data.Rational.Properties`.
 
@@ -606,7 +606,7 @@ Non-backwards compatible changes
   with the consequence that all arguments involving about accesibility and
   wellfoundedness proofs were polluted by almost-always-inferrable explicit
   arguments for the `y` position. The definition has now been changed to
-  make that argument *implicit*, as 
+  make that argument *implicit*, as
   ```agda
   WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
   WfRec _<_ P x = ∀ {y} → y < x → P y
@@ -931,40 +931,40 @@ Non-backwards compatible changes
   as would be expected. Instead it omitted several fields like irreflexivity as they were derivable from the
   proof of trichotomy. However, this led to problems further up the hierarchy where bundles such as `StrictTotalOrder`
   which contained multiple distinct proofs of `IsStrictPartialOrder`.
-  
-* To remedy this the definition of `IsStrictTotalOrder` has been changed to so that it builds upon 
-  `IsStrictPartialOrder` as would be expected. 
+
+* To remedy this the definition of `IsStrictTotalOrder` has been changed to so that it builds upon
+  `IsStrictPartialOrder` as would be expected.
 
 * To aid migration, the old record definition has been moved to `Relation.Binary.Structures.Biased`
-  which contains the `isStrictTotalOrderᶜ` smart constructor (which is re-exported by `Relation.Binary`) . 
+  which contains the `isStrictTotalOrderᶜ` smart constructor (which is re-exported by `Relation.Binary`) .
   Therefore the old code:
   ```agda
   <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
   <-isStrictTotalOrder = record
-	{ isEquivalence = isEquivalence
-	; trans         = <-trans
-	; compare       = <-cmp
-	}
+        { isEquivalence = isEquivalence
+        ; trans         = <-trans
+        ; compare       = <-cmp
+        }
   ```
   can be migrated either by updating to the new record fields if you have a proof of `IsStrictPartialOrder`
   available:
   ```agda
   <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
   <-isStrictTotalOrder = record
-	{ isStrictPartialOrder = <-isStrictPartialOrder
-	; compare              = <-cmp
-	}
+        { isStrictPartialOrder = <-isStrictPartialOrder
+        ; compare              = <-cmp
+        }
   ```
   or simply applying the smart constructor to the record definition as follows:
   ```agda
   <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
   <-isStrictTotalOrder = isStrictTotalOrderᶜ record
-	{ isEquivalence = isEquivalence
-	; trans         = <-trans
-	; compare       = <-cmp
-	}
+        { isEquivalence = isEquivalence
+        ; trans         = <-trans
+        ; compare       = <-cmp
+        }
   ```
-  
+
 ### Changes to triple reasoning interface
 
 * The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict
@@ -987,7 +987,7 @@ Non-backwards compatible changes
   Data.Vec.Relation.Binary.Lex.NonStrict
   Relation.Binary.Reasoning.StrictPartialOrder
   Relation.Binary.Reasoning.PartialOrder
-  ```	
+  ```
 
 ### Other
 
@@ -1165,7 +1165,7 @@ Non-backwards compatible changes
 * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to
   `¬¬-excluded-middle`.
 
-* `iterate` and `replicate` in `Data.Vec.Base` and `Data.Vec.Functional` 
+* `iterate` and `replicate` in `Data.Vec.Base` and `Data.Vec.Functional`
   now take the length of vector, `n`, as an explicit rather than an implicit argument.
   ```agda
   iterate : (A → A) → A → ∀ n → Vec A n
@@ -1231,11 +1231,11 @@ Major improvements
 
 ### More modular design of equational reasoning.
 
-* Have introduced a new module `Relation.Binary.Reasoning.Syntax` which exports 
+* Have introduced a new module `Relation.Binary.Reasoning.Syntax` which exports
   a range of modules containing pre-existing reasoning combinator syntax.
 
-* This makes it possible to add new or rename existing reasoning combinators to a 
-  pre-existing `Reasoning` module in just a couple of lines 
+* This makes it possible to add new or rename existing reasoning combinators to a
+  pre-existing `Reasoning` module in just a couple of lines
   (e.g. see `∣-Reasoning` in `Data.Nat.Divisibility`)
 
 Deprecated modules
@@ -1813,7 +1813,7 @@ Deprecated names
   ```agda
   _↔⟨⟩_  ↦  _≡⟨⟩_
   ```
-  
+
 * In `Foreign.Haskell.Either` and `Foreign.Haskell.Pair`:
   ```
   toForeign   ↦ Foreign.Haskell.Coerce.coerce
@@ -2706,7 +2706,7 @@ Additions to existing modules
   toℕ-inverseˡ  : Inverseˡ _≡_ _≡_ toℕ fromℕ
   toℕ-inverseʳ  : Inverseʳ _≡_ _≡_ toℕ fromℕ
   toℕ-inverseᵇ  : Inverseᵇ _≡_ _≡_ toℕ fromℕ
-  
+
   <-asym : Asymmetric _<_
   ```
 
@@ -3163,7 +3163,7 @@ Additions to existing modules
                 ∀ {m n} → _Respectsʳ_ (_<_ {m} {n}) _≋_
   <-wellFounded : Transitive _≈_ → _≺_ Respectsʳ _≈_ → WellFounded _≺_ →
                   ∀ {n} → WellFounded (_<_ {n})
-```
+  ```
 
 * Added new functions in `Data.Vec.Relation.Unary.Any`:
   ```
@@ -3190,9 +3190,9 @@ Additions to existing modules
 * Added new application operator synonym to `Function.Bundles`:
   ```agda
   _⟨$⟩_ : Func From To → Carrier From → Carrier To
-  _⟨$⟩_ = Func.to 
+  _⟨$⟩_ = Func.to
   ```
-  
+
 * Added new proofs in `Function.Construct.Symmetry`:
   ```
   bijective     : Bijective ≈₁ ≈₂ f → Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ f⁻¹
@@ -3888,7 +3888,7 @@ This is a full list of proofs that have changed form to use irrelevant instance
   blockerAll : List Blocker → Blocker
   blockTC : Blocker → TC A
   ```
-  
+
 * Added new file `Relation.Binary.Reasoning.Base.Apartness`
 
   This is how to use it:

src/Function/Bundles.agda

@@ -182,7 +182,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
 
     open Func toFunction public
       using (module Eq₁; module Eq₂)
-      renaming (isCongruent to to-isCongrunet)
+      renaming (isCongruent to to-isCongruent)
 
     fromFunction : Func To From
     fromFunction = record
@@ -192,7 +192,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
 
     open Func fromFunction public
       using ()
-      renaming (isCongruent to from-isCongrunet)
+      renaming (isCongruent to from-isCongruent)
 
 
   record LeftInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -481,7 +481,7 @@ module _ {A : Set a} {B : Set b} where
 
 module _ {From : Setoid a ℓ₁} {To : Setoid b ℓ₂} where
   open Setoid
-  
+
   infixl 5 _⟨$⟩_
   _⟨$⟩_ : Func From To → Carrier From → Carrier To
   _⟨$⟩_ = Func.to