diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9e34dba19a..7a36d5b1db 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -411,7 +411,7 @@ Non-backwards compatible changes
 * At the moment, there are 4 different ways such instance arguments can be provided,
   listed in order of convenience and clarity:
     1. *Automatic basic instances* - the standard library provides instances based on the constructors of each
-       numeric type in `Data.X.Base`. For example, `Data.Nat.Base` constains an instance of `NonZero (suc n)` for any `n`
+       numeric type in `Data.X.Base`. For example, `Data.Nat.Base` constrains an instance of `NonZero (suc n)` for any `n`
        and `Data.Integer.Base` contains an instance of `NonNegative (+ n)` for any `n`. Consequently,
        if the argument is of the required form, these instances will always be filled in by instance search
        automatically, e.g.
@@ -589,7 +589,7 @@ Non-backwards compatible changes
   ```
 
 * A new module `Reflection.AST` that re-exports the contents of the
-  submodules has been addeed.
+  submodules has been added.
 
 ### Implementation of division and modulus for `ℤ`
 
@@ -617,7 +617,7 @@ Non-backwards compatible changes
   * `IsSemiringWithoutAnnihilatingZero`
   * `IsRing`
 * To aid with migration, structures matching the old style ones have been added
-  to `Algebra.Structures.Biased`, with conversionFunctions:
+  to `Algebra.Structures.Biased`, with conversion functions:
   * `IsNearSemiring*` and `isNearSemiring*`
   * `IsSemiringWithoutOne*` and `isSemiringWithoutOne*`
   * `IsSemiringWithoutAnnihilatingZero*` and `isSemiringWithoutAnnihilatingZero*`
@@ -634,7 +634,7 @@ Non-backwards compatible changes
   ⊥ = Irrelevant Empty
   ```
   in order to make ⊥ proof irrelevant. Any two proofs of `⊥` or of a negated
-  statements are now *judgementally* equal to each other.
+  statements are now *judgmentally* equal to each other.
 
 * Consequently we have modified the following definitions:
   + In `Relation.Nullary.Decidable.Core`, the type of `dec-no` has changed
@@ -671,14 +671,14 @@ Non-backwards compatible changes
   however all their contents is re-exported by `Relation.Nullary` which is the easiest way to access
   it now.
 
-* In order to facilitate this reorganisation the following breaking moves have occured:
+* In order to facilitate this reorganisation the following breaking moves have occurred:
   - `¬?` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Decidable.Core`
   - `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Reflects`.
   - `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved from `Relation.Nullary.Negation`
     to `Relation.Nullary.Decidable`.
-  - `fromDec` and `toDec` have been mvoed from `Data.Sum.Base` to `Data.Sum`.
+  - `fromDec` and `toDec` have been moved from `Data.Sum.Base` to `Data.Sum`.
 
-### Refactoring of the unindexed Functor/Applicative/Monad hiearchy
+### Refactoring of the unindexed Functor/Applicative/Monad hierarchy
 
 * The unindexed versions are not defined in terms of the named versions anymore
 
@@ -698,7 +698,7 @@ Non-backwards compatible changes
 
 * `MonadT T` now returns a `MonadTd` record that packs both a proof that the
   `Monad M` transformed by `T` is a monad and that we can `lift` a computation
-  `M A` to a trasnformed computation `T M A`.
+  `M A` to a transformed computation `T M A`.
 
 * The monad transformer are not mere aliases anymore, they are record-wrapped
   which allows constraints such as `MonadIO (StateT S (ReaderT R IO))` to be
@@ -789,12 +789,12 @@ Non-backwards compatible changes
   previous implementation using the sum type `a ⟶ b ⊎ b ⟶ a`.
 
 * In `Algebra.Morphism.Structures`, `IsNearSemiringHomomorphism`,
-  `IsSemiringHomomorphism`, and `IsRingHomomorphism` have been redeisgned to
+  `IsSemiringHomomorphism`, and `IsRingHomomorphism` have been redesigned to
   build up from `IsMonoidHomomorphism`, `IsNearSemiringHomomorphism`, and
   `IsSemiringHomomorphism` respectively, adding a single property at each step.
   This means that they no longer need to have two separate proofs of
   `IsRelHomomorphism`. Similarly, `IsLatticeHomomorphism` is now built as
-  `IsRelHomomorphism` along with proofs that `_∧_` and `_∨_` are homorphic.
+  `IsRelHomomorphism` along with proofs that `_∧_` and `_∨_` are homomorphic.
 
   Also, `⁻¹-homo` in `IsRingHomomorphism` has been renamed to `-‿homo`.
 
@@ -939,7 +939,7 @@ Major improvements
 
 * To fix this, these operators have been moved to `Data.Nat.Base`. The properties
   for them still live in `Data.Nat.DivMod` (which also publicly re-exports them
-  to provide backwards compatability).
+  to provide backwards compatibility).
 
 * Beneficiaries of this change include `Data.Rational.Unnormalised.Base` whose
   dependencies are now significantly smaller.
@@ -1604,11 +1604,6 @@ New modules
   Data.List.NonEmpty.Relation.Unary.All
   ```
 
-* A small library for heterogenous equational reasoning on vectors:
-  ```
-  Data.Vec.Properties.Heterogeneous
-  ```
-
 * Show module for unnormalised rationals:
   ```
   Data.Rational.Unnormalised.Show