diff --git a/CHANGELOG.md b/CHANGELOG.md
index 95de9d08dd..d5851dde0d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,48 +1,54 @@
 Version 2.1-dev
 ===============
 
-The library has been tested using Agda 2.6.4, 2.6.4.1, and 2.6.4.3.
+The library has been tested using Agda 2.6.4.3.
 
 Highlights
 ----------
 
+* The size of the dependency graph for many modules has been
+  reduced. This may lead to speed ups for first-time loading of some
+  modules.
+
+* Added bindings for file handles in `IO.Handle`.
+
+* Added bindings for random number generation in `System.Random`
+
+* Added support for 8-bit words and bytestrings in `Data.Word8` and `Data.ByteString`.
+
 Bug-fixes
 ---------
 
-* Fix statement of `Data.Vec.Properties.toList-replicate`, where `replicate`
+* Fixed type of `toList-replicate` in `Data.Vec.Properties`, where `replicate`
   was mistakenly applied to the level of the type `A` instead of the
   variable `x` of type `A`.
 
 * Module `Data.List.Relation.Ternary.Appending.Setoid.Properties` no longer
-  exports the `Setoid` module under the alias `S`.
+  incorrectly publicly exports the `Setoid` module under the alias `S`.
 
-* Remove unbound parameter from `Data.List.Properties.length-alignWith`,
-  `alignWith-map` and `map-alignWith`.
+* Removed unbound parameter from `length-alignWith`,
+  `alignWith-map` and `map-alignWith` in `Data.List.Properties`.
 
 Non-backwards compatible changes
 --------------------------------
 
-* The modules and morphisms in `Algebra.Module.Morphism.Structures` are now
-  parametrized by _raw_ bundles rather than lawful bundles, in line with other
-  modules defining morphism structures.
-* The definitions in `Algebra.Module.Morphism.Construct.Composition` are now
-  parametrized by _raw_ bundles, and as such take a proof of transitivity.
-* The definitions in `Algebra.Module.Morphism.Construct.Identity` are now
-  parametrized by _raw_ bundles, and as such take a proof of reflexivity.
-* The module `IO.Primitive` was moved to `IO.Primitive.Core`.
-* The modules in the `Data.Word` hierarchy were moved to the `Data.Word64`
-  one instead.
+* The recently added modules and (therefore their contents) in:
+  ```agda
+  Algebra.Module.Morphism.Structures
+  Algebra.Module.Morphism.Construct.Composition
+  Algebra.Module.Morphism.Construct.Identity
+  ```
+  have been changed so they are now parametrized by _raw_ bundles rather
+  than lawful bundles.
+  This is in line with other modules that define morphisms.
+  As a result many of the `Composition` lemmas now take a proof of
+  transitivity and the `Identity` lemmas now take a proof of reflexivity.
 
-Other major improvements
-------------------------
+* The module `IO.Primitive` was moved to `IO.Primitive.Core`.
 
 Minor improvements
 ------------------
 
-* The size of the dependency graph for many modules has been
-  reduced. This may lead to speed ups for first-time loading of some
-  modules.
-
 * The definition of the `Pointwise` relational combinator in
   `Data.Product.Relation.Binary.Pointwise.NonDependent.Pointwise`
   has been generalised to take heterogeneous arguments in `REL`.
@@ -51,17 +57,25 @@ Minor improvements
   `Algebra.Lattice.Structures` have been redefined as aliases of
   `IsCommutativeBand` and `IsIdempotentMonoid` in `Algebra.Structures`.
 
-
 Deprecated modules
 ------------------
 
-* `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` deprecated in favour of
-  `Data.List.Relation.Binary.Sublist.Propositional.Slice`.
+* All modules in the `Data.Word` hierarchy have been deprecated in favour
+  of their newly introduced counterparts in `Data.Word64`.
+
+* The module `Data.List.Relation.Binary.Sublist.Propositional.Disjoint`
+  has been deprecated in favour of `Data.List.Relation.Binary.Sublist.Propositional.Slice`.
 
-* The modules `Function.Endomorphism.Propositional` and
-  `Function.Endomorphism.Setoid` that use the old `Function`
-  hierarchy. Use `Function.Endo.Propositional` and
-  `Function.Endo.Setoid` instead.
+* The modules
+  ```
+  Function.Endomorphism.Propositional
+  Function.Endomorphism.Setoid
+  ```
+  that used the old `Function` hierarchy have been deprecated in favour of:
+  ```
+  Function.Endo.Propositional
+  Function.Endo.Setoid
+  ```
 
 Deprecated names
 ----------------
@@ -76,17 +90,22 @@ Deprecated names
   _-_  ↦  _//_
   ```
 
-* In `Data.Maybe.Base`:
-  ```agda
-  decToMaybe  ↦  Relation.Nullary.Decidable.Core.dec⇒maybe
-  ```
-
 * In `Algebra.Structures.Biased`:
   ```agda
   IsRing*  ↦  Algebra.Structures.IsRing
   isRing*  ↦  Algebra.Structures.isRing
   ```
 
+* In `Data.Float.Base`:
+  ```agda
+  toWord ↦ toWord64
+  ```
+
+* In `Data.Float.Properties`:
+  ```agda
+  toWord-injective ↦ toWord64-injective
+  ```
+
 * In `Data.List.Base`:
   ```agda
   scanr  ↦  Data.List.Scans.Base.scanr
@@ -104,6 +123,11 @@ Deprecated names
   map-compose  ↦  map-∘
   ```
 
+* In `Data.Maybe.Base`:
+  ```agda
+  decToMaybe  ↦  Relation.Nullary.Decidable.Core.dec⇒maybe
+  ```
+
 * In `Data.Nat.Base`: the following pattern synonyms and definitions are all
   deprecated in favour of direct pattern matching on `Algebra.Definitions.RawMagma._∣ˡ_._,_`
   ```agda
@@ -111,7 +135,7 @@ Deprecated names
   pattern ≤″-offset k = k , refl
   pattern <″-offset k = k , refl
   s≤″s⁻¹
- ```
+  ```
 
 * In `Data.Nat.Divisibility.Core`:
   ```agda
@@ -129,16 +153,6 @@ Deprecated names
   untilRight  ↦  untilInj₂
   ```
 
-* In `Data.Float.Base`:
-  ```agda
-  toWord ↦ toWord64
-  ```
-
-* In `Data.Float.Properties`:
-  ```agda
-  toWord-injective ↦ toWord64-injective
-  ```
-
 New modules
 -----------
 
@@ -164,6 +178,16 @@ New modules
   Algebra.Morphism.Construct.Terminal
   ```
 
+* Bytestrings and builders:
+  ```agda
+  Data.Bytestring.Base
+  Data.Bytestring.Builder.Base
+  Data.Bytestring.Builder.Primitive
+  Data.Bytestring.IO
+  Data.Bytestring.IO.Primitive
+  Data.Bytestring.Primitive
+  ```
+
 * Pointwise and equality relations over indexed containers:
   ```agda
   Data.Container.Indexed.Relation.Binary.Pointwise
@@ -177,72 +201,66 @@ New modules
   Data.List.Scans.Properties
   ```
 
+* Various show modules for lists and vector types:
+  ```agda
+  Data.List.Show
+  Data.Vec.Show
+  Data.Vec.Bounded.Show
+  ```
+
 * Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid):
   ```
   Data.List.Relation.Binary.Equality.Setoid.Properties
   ```
 
-* `Data.List.Relation.Binary.Sublist.Propositional.Slice`
-  replacing `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` (*)
-  and adding new functions:
-  - `⊆-upper-bound-is-cospan` generalising `⊆-disjoint-union-is-cospan` from (*)
-  - `⊆-upper-bound-cospan` generalising `⊆-disjoint-union-cospan` from (*)
-  ```
-
-* Prime factorisation of natural numbers.
-  ```
-  Data.Nat.Primality.Factorisation
+* Decidability for the subset relation on lists:
+  ```agda
+  Data.List.Relation.Binary.Subset.DecSetoid (_⊆?_)
+  Data.List.Relation.Binary.Subset.DecPropositional
   ```
 
-* `Data.Vec.Functional.Relation.Binary.Permutation`, defining:
+* Decidability for the disjoint relation on lists:
   ```agda
-  _↭_ : IRel (Vector A) _
+  Data.List.Relation.Binary.Disjoint.DecSetoid (disjoint?)
+  Data.List.Relation.Binary.Disjoint.DecPropositional
   ```
 
-* `Data.Vec.Functional.Relation.Binary.Permutation.Properties` of the above:
+* Prime factorisation of natural numbers.
   ```agda
-  ↭-refl      : Reflexive (Vector A) _↭_
-  ↭-reflexive : xs ≡ ys → xs ↭ ys
-  ↭-sym       : Symmetric (Vector A) _↭_
-  ↭-trans     : Transitive (Vector A) _↭_
-  isIndexedEquivalence : {A : Set a} → IsIndexedEquivalence (Vector A) _↭_
-  indexedSetoid        : {A : Set a} → IndexedSetoid ℕ a _
+  Data.Nat.Primality.Factorisation
   ```
 
-* The modules `Function.Endo.Propositional` and
-  `Function.Endo.Setoid` are new but are actually proper ports of
-  `Function.Endomorphism.Propositional` and
-  `Function.Endomorphism.Setoid`.
-
-* `Function.Relation.Binary.Equality`
+* Permutations of vectors as functions:
   ```agda
-  setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
+  Data.Vec.Functional.Relation.Binary.Permutation
+  Data.Vec.Functional.Relation.Binary.Permutation.Properties
   ```
-  and a convenient infix version
+
+* A type of bytes:
   ```agda
-  _⇨_ = setoid
+  Data.Word8.Primitive
+  Data.Word8.Base
+  Data.Word8.Literals
+  Data.Word8.Show
   ```
 
-* Consequences of 'infinite descent' for (accessible elements of) well-founded relations:
+* Word64 literals and bit-based functions:
   ```agda
-  Induction.InfiniteDescent
+  Data.Word64.Literals
+  Data.Word64.Unsafe
+  Data.Word64.Show
   ```
 
-* Symmetric interior of a binary relation
-  ```
-  Relation.Binary.Construct.Interior.Symmetric
-  ```
 
-* Properties of `Setoid`s with decidable equality relation:
+* Pointwise equality over functions
   ```
-  Relation.Binary.Properties.DecSetoid
+  Function.Relation.Binary.Equality`
   ```
 
-* Systematise the use of `Recomputable A = .A → A`:
+* Consequences of 'infinite descent' for (accessible elements of) well-founded relations:
   ```agda
-  Relation.Nullary.Recomputable
+  Induction.InfiniteDescent
   ```
-  with `Recomputable` exported publicly from `Relation.Nullary`.
 
 * New IO primitives to handle buffering
   ```agda
@@ -250,60 +268,32 @@ New modules
   IO.Handle
   ```
 
-* `System.Random` bindings:
-  ```agda
-  System.Random.Primitive
-  System.Random
-  ```
-
-* Show modules:
-  ```agda
-  Data.List.Show
-  Data.Vec.Show
-  Data.Vec.Bounded.Show
+* Symmetric interior of a binary relation
   ```
-
-* Word64 literals and bit-based functions:
-  ```agda
-  Data.Word64.Literals
-  Data.Word64.Unsafe
-  Data.Word64.Show
+  Relation.Binary.Construct.Interior.Symmetric
   ```
 
-* A type of bytes:
-  ```agda
-  Data.Word8.Primitive
-  Data.Word8.Base
-  Data.Word8.Literals
-  Data.Word8.Show
+* Properties of `Setoid`s with decidable equality relation:
   ```
-
-* Bytestrings and builders:
-  ```agda
-  Data.Bytestring.Base
-  Data.Bytestring.Builder.Base
-  Data.Bytestring.Builder.Primitive
-  Data.Bytestring.IO
-  Data.Bytestring.IO.Primitive
-  Data.Bytestring.Primitive
+  Relation.Binary.Properties.DecSetoid
   ```
 
-* Decidability for the subset relation on lists:
+* Collection of results about recomputability in
   ```agda
-  Data.List.Relation.Binary.Subset.DecSetoid (_⊆?_)
-  Data.List.Relation.Binary.Subset.DecPropositional
+  Relation.Nullary.Recomputable
   ```
+  with the main definition `Recomputable` exported publicly from `Relation.Nullary`.
 
-* Decidability for the disjoint relation on lists:
+* New bindings to random numbers:
   ```agda
-  Data.List.Relation.Binary.Disjoint.DecSetoid (disjoint?)
-  Data.List.Relation.Binary.Disjoint.DecPropositional
+  System.Random.Primitive
+  System.Random
   ```
 
 Additions to existing modules
 -----------------------------
 
-* In `Algebra.Bundles`
+* Added new definitions in `Algebra.Bundles`:
   ```agda
   record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ))
   record CommutativeBand c ℓ : Set (suc (c ⊔ ℓ))
@@ -315,28 +305,21 @@ Additions to existing modules
   IdempotentSemiring
   ```
 
-
-* In `Algebra.Bundles.Raw`
+* Added new definition in `Algebra.Bundles.Raw`
   ```agda
   record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ))
   ```
 
-* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`:
-  ```agda
-  rawNearSemiring   : RawNearSemiring _ _
-  rawRingWithoutOne : RawRingWithoutOne _ _
-  +-rawGroup        : RawGroup _ _
-  ```
-
-* In `Algebra.Construct.Terminal`:
+* Added new proofs in `Algebra.Construct.Terminal`:
   ```agda
   rawNearSemiring : RawNearSemiring c ℓ
   nearSemiring    : NearSemiring c ℓ
   ```
 
-* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts.
+* In `Algebra.Module.Bundles`, raw bundles are now re-exported and bundles
+  consistently expose their raw counterparts.
 
-* In `Algebra.Module.Construct.DirectProduct`:
+* Added proofs in `Algebra.Module.Construct.DirectProduct`:
   ```agda
   rawLeftSemimodule  : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
   rawLeftModule      : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
@@ -348,7 +331,7 @@ Additions to existing modules
   rawModule          : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
   ```
 
-* In `Algebra.Module.Construct.TensorUnit`:
+* Added proofs in `Algebra.Module.Construct.TensorUnit`:
   ```agda
   rawLeftSemimodule  : RawLeftSemimodule _ c ℓ
   rawLeftModule      : RawLeftModule _ c ℓ
@@ -360,7 +343,7 @@ Additions to existing modules
   rawModule          : RawModule _ c ℓ
   ```
 
-* In `Algebra.Module.Construct.Zero`:
+* Added proofs in `Algebra.Module.Construct.Zero`:
   ```agda
   rawLeftSemimodule  : RawLeftSemimodule R c ℓ
   rawLeftModule      : RawLeftModule R c ℓ
@@ -372,23 +355,23 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
-* In `Algebra.Morphism.Structures`:
+* Added definitions in `Algebra.Morphism.Structures`:
   ```agda
-  module SuccessorSetMorphisms (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂) where
-    record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
-    record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
-    record IsSuccessorSetIsomorphism  (⟦_⟧ : N₁.Carrier →  N₂.Carrier) : Set _
+  record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
+  record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
+  record IsSuccessorSetIsomorphism  (⟦_⟧ : N₁.Carrier →  N₂.Carrier) : Set _
 
   IsSemigroupHomomorphism : (A → B) → Set _
   IsSemigroupMonomorphism : (A → B) → Set _
   IsSemigroupIsomorphism : (A → B) → Set _
   ```
-* In `Algebra.Properties.AbelianGroup`:
+
+* Added proof in `Algebra.Properties.AbelianGroup`:
   ```
   ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x
   ```
 
-* In `Algebra.Properties.Group`:
+* Added proofs in `Algebra.Properties.Group`:
   ```agda
   isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
   quasigroup      : Quasigroup _ _
@@ -411,52 +394,42 @@ Additions to existing modules
   ⁻¹-anti-homo-\\ : (x \\ y) ⁻¹ ≈ y \\ x
   ```
 
-* In `Algebra.Properties.Loop`:
+* Added new proofs in `Algebra.Properties.Loop`:
   ```agda
   identityˡ-unique : x ∙ y ≈ y → x ≈ ε
   identityʳ-unique : x ∙ y ≈ x → y ≈ ε
   identity-unique  : Identity x _∙_ → x ≈ ε
   ```
 
-* In `Algebra.Properties.Monoid.Mult`:
+* Added new proofs in `Algebra.Properties.Monoid.Mult`:
   ```agda
-  ×-homo-0 : ∀ x → 0 × x ≈ 0#
-  ×-homo-1 : ∀ x → 1 × x ≈ x
+  ×-homo-0 : 0 × x ≈ 0#
+  ×-homo-1 : 1 × x ≈ x
   ```
 
-* In `Algebra.Properties.Semiring.Mult`:
+* Added new proofs in `Algebra.Properties.Semiring.Mult`:
   ```agda
-  ×-homo-0#     : ∀ x → 0 × x ≈ 0# * x
-  ×-homo-1#     : ∀ x → 1 × x ≈ 1# * x
+  ×-homo-0#     : 0 × x ≈ 0# * x
+  ×-homo-1#     : 1 × x ≈ 1# * x
   idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
   ```
 
-* In `Algebra.Structures`
+* Added new definitions to `Algebra.Structures`:
   ```agda
   record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _
   record IsCommutativeBand (∙ : Op₂ A) : Set _
   record IsIdempotentMonoid (∙ : Op₂ A) (ε : A) : Set _
   ```
-  and additional manifest fields for substructures arising from these in:
-  ```agda
-  IsIdempotentCommutativeMonoid
-  IsIdempotentSemiring
-  ```
 
-* In `Algebra.Structures.IsGroup`:
+* Added new definitions in `IsGroup` record in `Algebra.Structures`:
   ```agda
-  infixl 6 _//_
-  _//_ : Op₂ A
   x // y = x ∙ (y ⁻¹)
-  infixr 6 _\\_
-  _\\_ : Op₂ A
   x \\ y = (x ⁻¹) ∙ y
   ```
 
-* In `Algebra.Structures.IsCancellativeCommutativeSemiring` add the
-  extra property as an exposed definition:
+* In `Algebra.Structures` added new proof to `IsCancellativeCommutativeSemiring` record:
   ```agda
-    *-cancelʳ-nonZero : AlmostRightCancellative 0# *
+  *-cancelʳ-nonZero : AlmostRightCancellative 0# *
   ```
 
 * In `Data.Bool.Show`:
@@ -484,7 +457,7 @@ Additions to existing modules
   _≤_ : Rel Float _
   ```
 
-* In `Data.Integer.Divisibility`: introduce `divides` as an explicit pattern synonym
+* In `Data.Integer.Divisibility` introduced `divides` as an explicit pattern synonym
   ```agda
   pattern divides k eq = Data.Nat.Divisibility.divides k eq
   ```
@@ -496,11 +469,12 @@ Additions to existing modules
   i*j≢0     : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
   ```
 
-* In `Data.List.Base` redefine `inits` and `tails` in terms of:
+* In `Data.List.Base` added two new functions:
   ```agda
   Inits.tail : List A → List (List A)
   Tails.tail : List A → List (List A)
   ```
+  and redefined `inits` and `tails` in terms of them.
 
 * In `Data.List.Membership.Propositional.Properties.Core`:
   ```agda
@@ -514,18 +488,6 @@ Additions to existing modules
   reverse⁻ : x ∈ reverse xs → x ∈ xs
   ```
 
-* In `Data.List.NonEmpty.Base`:
-  ```agda
-  inits : List A → List⁺ (List A)
-  tails : List A → List⁺ (List A)
-  ```
-
-* In `Data.List.NonEmpty.Properties`:
-  ```agda
-  toList-inits : toList ∘ List⁺.inits ≗ List.inits
-  toList-tails : toList ∘ List⁺.tails ≗ List.tails
-  ```
-
 * In `Data.List.Properties`:
   ```agda
   length-catMaybes       : length (catMaybes xs) ≤ length xs
@@ -584,11 +546,6 @@ Additions to existing modules
   unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S)
   ```
 
-* In `Data.Maybe.Relation.Binary.Pointwise`:
-  ```agda
-  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
-  ```
-
 * In `Data.List.Relation.Binary.Sublist.Setoid`:
   ```agda
   ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ
@@ -606,15 +563,6 @@ Additions to existing modules
                   ⊆-trans ps (⊆-trans qs rs) ≡ ⊆-trans (⊆-trans ps qs) rs
   ```
 
-* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
-  ```agda
-  map⁺ : f Preserves _≈_ ⟶ _≈′_ → as ⊆ bs → map f as ⊆′ map f bs
-
-  reverse-selfAdjoint : as ⊆ reverse bs → reverse as ⊆ bs
-  reverse⁺            : as ⊆ bs → reverse as ⊆ reverse bs
-  reverse⁻            : reverse as ⊆ reverse bs → as ⊆ bs
-  ```
-
 * In `Data.List.Relation.Unary.All`:
   ```agda
   universal-U : Universal (All U)
@@ -638,6 +586,34 @@ Additions to existing modules
              (p : Any P xs) → Any.map f p ≡ Any.map g p
   ```
 
+* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
+  ```agda
+  product-↭   : product Preserves _↭_ ⟶ _≡_
+  catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
+  mapMaybe-↭  : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
+  ```
+
+* Added new proofs to `Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe`:
+  ```agda
+  catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
+  mapMaybe-↭  : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
+  ```
+
+* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
+  ```agda
+  map⁺ : f Preserves _≈_ ⟶ _≈′_ → as ⊆ bs → map f as ⊆′ map f bs
+
+  reverse-selfAdjoint : as ⊆ reverse bs → reverse as ⊆ bs
+  reverse⁺            : as ⊆ bs → reverse as ⊆ reverse bs
+  reverse⁻            : reverse as ⊆ reverse bs → as ⊆ bs
+  ```
+
+* Added new proofs to `Data.List.Relation.Binary.Sublist.Propositional.Slice`:
+  ```agda
+  ⊆-upper-bound-is-cospan : (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → IsCospan (⊆-upper-bound τ₁ τ₂)
+  ⊆-upper-bound-cospan    : (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → Cospan τ₁ τ₂
+  ```
+
 * In `Data.List.Relation.Ternary.Appending.Setoid.Properties`:
   ```agda
   through→ : ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs →
@@ -664,6 +640,23 @@ Additions to existing modules
                          ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds
   ```
 
+* In `Data.List.NonEmpty.Base`:
+  ```agda
+  inits : List A → List⁺ (List A)
+  tails : List A → List⁺ (List A)
+  ```
+
+* In `Data.List.NonEmpty.Properties`:
+  ```agda
+  toList-inits : toList ∘ List⁺.inits ≗ List.inits
+  toList-tails : toList ∘ List⁺.tails ≗ List.tails
+  ```
+
+* In `Data.Maybe.Relation.Binary.Pointwise`:
+  ```agda
+  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
+  ```
+
 * In `Data.Nat.Divisibility`:
   ```agda
   quotient≢0       : m ∣ n → .{{NonZero n}} → NonZero quotient
@@ -681,10 +674,17 @@ Additions to existing modules
   nonZeroDivisor : DivMod dividend divisor → NonZero divisor
   ```
 
+* Added new proofs to `Data.Nat.Primality`:
+  ```agda
+  rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n
+  productOfPrimes≢0 : All Prime as → NonZero (product as)
+  productOfPrimes≥1 : All Prime as → product as ≥ 1
+  ```
+
 * Added new proofs in `Data.Nat.Properties`:
   ```agda
-  m≤n+o⇒m∸n≤o    : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o
-  m<n+o⇒m∸n<o    : ∀ m n {o} → .{{NonZero o}} → m < n + o → m ∸ n < o
+  m≤n+o⇒m∸n≤o    : m ≤ n + o → m ∸ n ≤ o
+  m<n+o⇒m∸n<o    : .{{NonZero o}} → m < n + o → m ∸ n < o
   pred-cancel-≤  : pred m ≤ pred n → (m ≡ 1 × n ≡ 0) ⊎ m ≤ n
   pred-cancel-<  : pred m < pred n → m < n
   pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
@@ -695,26 +695,6 @@ Additions to existing modules
   guarded-∸≗∸   : .(m≤n : m ≤ n) → let k , _ = m≤n⇒∃[o]m+o≡n m≤n in k ≡ n ∸ m
   ```
 
-* Added new proofs to `Data.Nat.Primality`:
-  ```agda
-  rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n
-  productOfPrimes≢0 : All Prime as → NonZero (product as)
-  productOfPrimes≥1 : All Prime as → product as ≥ 1
-  ```
-
-* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
-  ```agda
-  product-↭   : product Preserves _↭_ ⟶ _≡_
-  catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
-  mapMaybe-↭  : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
-  ```
-
-* Added new proofs to `Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe`:
-  ```agda
-  catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
-  mapMaybe-↭  : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
-  ```
-
 * Added some very-dependent map and zipWith to `Data.Product`.
   ```agda
   map-Σ : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} →
@@ -729,7 +709,6 @@ Additions to existing modules
     (_*_ : (x : C) → (y : R x) → S x y) →
     ((a , p) : Σ A P) → ((b , q) : Σ B Q) →
         S (a ∙ b) (p ∘ q)
-
   ```
 
 * In `Data.Rational.Properties`:
@@ -751,6 +730,21 @@ Additions to existing modules
   between : String → String → String → String
   ```
 
+* Added new functions in `Data.Vec.Bounded.Base`:
+  ```agda
+  isBounded : (as : Vec≤ A n) → Vec≤.length as ≤ n
+  toVec     : (as : Vec≤ A n) → Vec A (Vec≤.length as)
+  ```
+
+* In `Data.Word64.Base`:
+  ```agda
+  _≤_ : Rel Word64 zero
+  show : Word64 → String
+  ```
+
+* In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can
+  be used infix.
+
 * Re-exported new types and functions in `IO`:
   ```agda
   BufferMode : Set
@@ -777,38 +771,18 @@ Additions to existing modules
   _>>_ : IO A → IO B → IO B
   ```
 
-* In `Data.Word64.Base`:
-  ```agda
-  _≤_ : Rel Word64 zero
-  show : Word64 → String
-  ```
-
 * Added new definition in `Relation.Binary.Construct.Closure.Transitive`
   ```agda
   transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_
   ```
 
-* Added new definition in `Relation.Unary`
-  ```
-  Stable : Pred A ℓ → Set _
-  ```
-
-* Added new functions in `Data.Vec.Bounded.Base`:
-  ```agda
-  isBounded : (as : Vec≤ A n) → Vec≤.length as ≤ n
-  toVec     : (as : Vec≤ A n) → Vec A (Vec≤.length as)
-  ```
-
-* In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can
-  be used infix.
-
 * Added new proofs in `Relation.Binary.Construct.Composition`:
   ```agda
   transitive⇒≈;≈⊆≈ : Transitive ≈ → (≈ ; ≈) ⇒ ≈
   ```
 
 * Added new definitions in `Relation.Binary.Definitions`
-  ```
+  ```agda
   Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y)
   Empty  _∼_ = ∀ {x y} → ¬ (x ∼ y)
   ```
@@ -821,22 +795,22 @@ Additions to existing modules
   ```
 
 * Added new definitions in `Relation.Nullary`
-  ```
+  ```agda
   Recomputable    : Set _
   WeaklyDecidable : Set _
   ```
 
-* Added new definition and proof in `Relation.Nullary.Decidable.Core`:
+* Added new proof in `Relation.Nullary.Decidable`:
   ```agda
-  dec⇒maybe : Dec A → Maybe A
-  recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
-  toSum              : Dec A → A ⊎ ¬ A
-  fromSum            : A ⊎ ¬ A → Dec A
+  ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
   ```
 
-* Added new proof in `Relation.Nullary.Decidable`:
+* Added new definitions and proofs in `Relation.Nullary.Decidable.Core`:
   ```agda
-  ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
+  dec⇒maybe          : Dec A → Maybe A
+  recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
+  toSum              : Dec A → A ⊎ ¬ A
+  fromSum            : A ⊎ ¬ A → Dec A
   ```
 
 * Added new definitions in `Relation.Nullary.Negation.Core`:
@@ -851,7 +825,7 @@ Additions to existing modules
  ```
 
 * Added new definitions in `Relation.Unary`
-  ```
+  ```agda
   Stable          : Pred A ℓ → Set _
   WeaklyDecidable : Pred A ℓ → Set _
   ```
diff --git a/agda-stdlib-utils.cabal b/agda-stdlib-utils.cabal
index bbd7e4f118..d9fe1dc676 100644
--- a/agda-stdlib-utils.cabal
+++ b/agda-stdlib-utils.cabal
@@ -1,6 +1,6 @@
 cabal-version:   2.4
 name:            agda-stdlib-utils
-version:         2.0
+version:         2.1
 build-type:      Simple
 description:     Helper programs for setting up the Agda standard library.
 license:         MIT