Merge tag 'upstream/0.17'

Upstream version 0.17 # gpg: Signature made Fri 23 Nov 2018 05:29:18 PM MST # gpg: using RSA key 9B917007AE030E36E4FC248B695B7AE4BF066240 # gpg: issuer "spwhitton@spwhitton.name" # gpg: Good signature from "Sean Whitton <spwhitton@spwhitton.name>" [ultimate] # Primary key fingerprint: 8DC2 487E 51AB DD90 B5C4 753F 0F56 D055 3B6D 411B # Subkey fingerprint: 9B91 7007 AE03 0E36 E4FC 248B 695B 7AE4 BF06 6240
author: Sean Whitton <spwhitton@spwhitton.name> 2018-11-23 17:29:46 -0700
committer: Sean Whitton <spwhitton@spwhitton.name> 2018-11-23 17:29:46 -0700
commit: 5a91775bd7c909bbaf3b3c8ee964136961a5146d (patch)
tree: cea89f085c1382f1567ff71a30b6f953708dc6a9 /CHANGELOG
parent: 5d2b156377dce5bdca65b14639306eaed3ac3a92 (diff)
parent: a19b25a865b2000bbd3acd909f5951a5407c1eec (diff)
17 files changed, 2531 insertions, 0 deletions
diff --git a/CHANGELOG/v0.01.md b/CHANGELOG/v0.01.md
new file mode 100644
index 0000000..e311ae9
--- /dev/null
+++ b/CHANGELOG/v0.01.md
@@ -0,0 +1,8 @@
+Version 0.1
+===========
+
+Version 0.1 of the
+["standard" library](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary)
+has now been released.
+
+The library has been tested using Agda version 2.2.2.
diff --git a/CHANGELOG/v0.02.md b/CHANGELOG/v0.02.md
new file mode 100644
index 0000000..1343288
--- /dev/null
+++ b/CHANGELOG/v0.02.md
@@ -0,0 +1,11 @@
+Version 0.2
+===========
+
+Version 0.2 of the
+["standard" library](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary)
+has now been released.
+
+The library has been tested using Agda version 2.2.4.
+
+Note that the library sources are now located in the sub-directory
+`lib-<version>/src` of the installation tarball.
diff --git a/CHANGELOG/v0.03.md b/CHANGELOG/v0.03.md
new file mode 100644
index 0000000..b0a2853
--- /dev/null
+++ b/CHANGELOG/v0.03.md
@@ -0,0 +1,8 @@
+Version 0.3
+===========
+
+Version 0.3 of the
+[standard library](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary)
+has now been released.
+
+The library has been tested using Agda version 2.2.6.
diff --git a/CHANGELOG/v0.04.md b/CHANGELOG/v0.04.md
new file mode 100644
index 0000000..925bced
--- /dev/null
+++ b/CHANGELOG/v0.04.md
@@ -0,0 +1,8 @@
+Version 0.4
+===========
+
+Version 0.4 of the
+[standard library](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary)
+has now been released.
+
+The library has been tested using Agda version 2.2.8.
diff --git a/CHANGELOG/v0.05.md b/CHANGELOG/v0.05.md
new file mode 100644
index 0000000..67a66a6
--- /dev/null
+++ b/CHANGELOG/v0.05.md
@@ -0,0 +1,8 @@
+Version 0.5
+===========
+
+Version 0.5 of the
+[standard library](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary)
+has now been released.
+
+The library has been tested using Agda version 2.2.10.
diff --git a/CHANGELOG/v0.06.md b/CHANGELOG/v0.06.md
new file mode 100644
index 0000000..27058d0
--- /dev/null
+++ b/CHANGELOG/v0.06.md
@@ -0,0 +1,8 @@
+Version 0.6
+===========
+
+Version 0.6 of the
+[standard library](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary)
+has now been released.
+
+The library has been tested using Agda version 2.3.0.
diff --git a/CHANGELOG/v0.07.md b/CHANGELOG/v0.07.md
new file mode 100644
index 0000000..b90e50f
--- /dev/null
+++ b/CHANGELOG/v0.07.md
@@ -0,0 +1,8 @@
+Version 0.7
+===========
+
+Version 0.7 of the
+[standard library](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary)
+has now been released.
+
+The library has been tested using Agda version 2.3.2.
diff --git a/CHANGELOG/v0.08.1.md b/CHANGELOG/v0.08.1.md
new file mode 100644
index 0000000..48a9f67
--- /dev/null
+++ b/CHANGELOG/v0.08.1.md
@@ -0,0 +1,20 @@
+Version 0.8.1
+=============
+
+The library has been tested using Agda version 2.4.2.
+
+Important changes since 0.8:
+
+* Reflection API
+
+  Agda 2.4.2 added support for literals, function definitions, pattern
+  matching lambdas and absurd clause/patterns (see Agda release
+  notes). The new supported entities were added to the
+  `Reflection.agda` module.
+
+* Modules renamed
+
+  `Foo.Props.Bar` -> `Foo.Properties.Bar`
+
+  The current compatibility modules `Foo.Props.Bar` will be removed in
+  the next release.
diff --git a/CHANGELOG/v0.08.md b/CHANGELOG/v0.08.md
new file mode 100644
index 0000000..b5af4ba
--- /dev/null
+++ b/CHANGELOG/v0.08.md
@@ -0,0 +1,8 @@
+Version 0.8
+===========
+
+Version 0.8 of the
+[standard library](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary)
+has now been released.
+
+The library has been tested using Agda version 2.4.0.
diff --git a/CHANGELOG/v0.09.md b/CHANGELOG/v0.09.md
new file mode 100644
index 0000000..31dce8b
--- /dev/null
+++ b/CHANGELOG/v0.09.md
@@ -0,0 +1,29 @@
+Version 0.9
+===========
+
+The library has been tested using Agda version 2.4.2.1.
+
+Important changes since 0.8.1:
+
+* `Data.List.NonEmpty`
+
+  Non-empty lists are no longer defined in terms of
+  `Data.Product._×_`, instead, now they are defined as record with
+  fields head and tail.
+
+* Reflection API
+
+  + Quoting levels was fixed. This fix could break some code (see Agda
+    Issue [#1207](https://github.com/agda/agda/issues/1269)).
+
+  + The `Reflection.type` function returns a normalised
+    `Reflection.Type` and `quoteTerm` returns an η-contracted
+    `Reflection.Term` now. These changes could break some code (see
+    Agda Issue [#1269](https://github.com/agda/agda/issues/1269)).
+
+  + The primitive function for showing names, `primShowQName`, is now
+    exposed as `Reflection.showName`.
+
+* Removed compatibility modules for `Props -> Properties` rename
+
+  Use `Foo.Properties.Bar` instead of `Foo.Props.Bar`.
diff --git a/CHANGELOG/v0.10.md b/CHANGELOG/v0.10.md
new file mode 100644
index 0000000..4eb6630
--- /dev/null
+++ b/CHANGELOG/v0.10.md
@@ -0,0 +1,148 @@
+Version 0.10
+============
+
+The library has been tested using Agda version 2.4.2.3.
+
+Important changes since 0.9:
+
+* Renamed `Data.Unit.Core` to `Data.Unit.NonEta`.
+
+* Removed `Data.String.Core`. The module `Data.String.Base` now
+  contains these definitions.
+
+* Removed `Relation.Nullary.Core`. The module `Relation.Nullary` now
+  contains these definitions directly.
+
+* Inspect on steroids has been simplified (see
+  `Relation.Binary.PropositionalEquality` and
+  `Relation.Binary.HeterogeneousEquality`).
+
+  The old version has been deprecated (see the above modules) and it
+  will be removed in the next release.
+
+* Using `Data.X.Base` modules.
+
+  The `Data.X.Base` modules are used for cheaply importing a data type
+  and the most common definitions. The use of these modules reduce
+  type-checking and compilation times.
+
+  At the moment, the modules added are:
+
+  ```agda
+  Data.Bool.Base
+  Data.Char.Base
+  Data.Integer.Base
+  Data.List.Base
+  Data.Maybe.Base
+  Data.Nat.Base
+  Data.String.Base
+  Data.Unit.Base
+  ```
+
+  These modules are also cheap to import and can be considered basic:
+
+  ```agda
+  Data.BoundedVec.Inefficient
+  Data.Empty
+  Data.Product
+  Data.Sign
+  Data.Sum
+  Function
+  Level
+  Relation.Binary
+  Relation.Binary.PropositionalEquality.TrustMe
+  Relation.Nullary
+  ```
+
+* Added singleton sets to `Relation.Unary`.
+
+  There used to be an isomorphic definition of singleton sets in
+  `Monad.Predicate`, this has been removed and the module has been
+  cleaned up accordingly.
+
+  The singleton set is also used to define generic operations (Plotkin
+  and Power's terminology) in `Data.Container.Indexed.FreeMonad`.
+
+* Proved properties of `Data.List.gfilter`. The following definitions
+  have been added to Data.List.Properties:
+
+  ```agda
+  gfilter-just      : ... → gfilter just xs ≡ xs
+  gfilter-nothing   : ... → gfilter (λ _ → nothing) xs ≡ []
+  gfilter-concatMap : ... → gfilter f ≗ concatMap (fromMaybe ∘ f)
+  ```
+
+* New in `Data.Nat.Properties`:
+
+  ```agda
+  <⇒≤pred : ∀ {m n} → m < n → m ≤ pred n
+  ```
+
+* New in `Data.Fin`:
+
+  ```agda
+  strengthen : ∀ {n} (i : Fin n) → Fin′ (suc i)
+  ```
+
+* New in `Data.Fin.Properties`:
+
+  ```agda
+  from-to        : ∀ {n} (i : Fin n) → fromℕ (toℕ i) ≡ strengthen i
+  toℕ-strengthen : ∀ {n} (i : Fin n) → toℕ (strengthen i) ≡ toℕ i
+
+  fromℕ-def    : ∀ n → fromℕ n ≡ fromℕ≤ ℕ≤-refl
+  reverse-suc  : ∀{n}{i : Fin n} → toℕ (reverse (suc i)) ≡ toℕ (reverse i)
+  inject≤-refl : ∀ {n} (i : Fin n) (n≤n : n ℕ≤ n) → inject≤ i n≤n ≡ i
+  ```
+
+* New in `Data.List.NonEmpty`:
+
+  ```agda
+  foldr₁ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
+  foldl₁ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
+  ```
+
+* `Data.AVL.Height-invariants._∼_` was replaced by `_∼_⊔_`, following
+  Conor McBride's principle of pushing information into indices rather
+  than pulling information out.
+
+  Some lemmas in `Data.AVL.Height-invariants` (`1+`, `max∼max` and
+  `max-lemma`) were removed.
+
+  The implementations of some functions in `Data.AVL` were simplified.
+  This could mean that they, and other functions depending on them (in
+  `Data.AVL`, `Data.AVL.IndexedMap` and `Data.AVL.Sets`), reduce in a
+  different way than they used to.
+
+* The fixity of all `_∎` and `finally` operators, as well as
+  `Category.Monad.Partiality.All._⟨_⟩P`, was changed from `infix 2` to
+  `infix 3`.
+
+* The fixity of `Category.Monad.Partiality._≟-Kind_`, `Data.AVL._∈?_`,
+  `Data.AVL.IndexedMap._∈?_`, `Data.AVL.Sets._∈?_`, `Data.Bool._≟_`,
+  `Data.Char._≟_`, `Data.Float._≟_`, `Data.Nat._≤?_`,
+  `Data.Nat.Divisibility._∣?_`, `Data.Sign._≟_`, `Data.String._≟_`,
+  `Data.Unit._≟_`, `Data.Unit._≤?_` and
+  `Data.Vec.Equality.DecidableEquality._≟_` was changed from the
+  default to `infix 4`.
+
+* The fixity of all `_≟<something>_` operators in `Reflection` is now
+  `infix 4` (some of them already had this fixity).
+
+* The fixity of `Algebra.Operations._×′_` was changed from the default
+  to `infixr 7`.
+
+* The fixity of `Data.Fin.#_` was changed from the default to
+  `infix 10`.
+
+* The fixity of `Data.Nat.Divisibility.1∣_` and `_∣0` was changed from
+  the default to `infix 10`.
+
+* The fixity of `Data.Nat.DivMod._divMod_`, `_div_` and `_mod_` was
+  changed from the default to `infixl 7`.
+
+* The fixity of `Data.Product.Σ-syntax` was changed from the default
+  to `infix 2`.
+
+* The fixity of `Relation.Unary._~` was changed from the default to
+  `infix 10`.
diff --git a/CHANGELOG/v0.11.md b/CHANGELOG/v0.11.md
new file mode 100644
index 0000000..b6850a8
--- /dev/null
+++ b/CHANGELOG/v0.11.md
@@ -0,0 +1,19 @@
+Version 0.11
+============
+
+The library has been tested using Agda version 2.4.2.4.
+
+Important changes since 0.10:
+
+* `Relation.Binary.PropositionalEquality.TrustMe.erase` was added.
+
+* Added `Data.Nat.Base.{_≤″_,_≥″_,_<″_,_>″_,erase}`,
+  `Data.Nat.Properties.{≤⇒≤″,≤″⇒≤}`, `Data.Fin.fromℕ≤″`, and
+  `Data.Fin.Properties.fromℕ≤≡fromℕ≤″`.
+
+* The functions in `Data.Nat.DivMod` have been optimised.
+
+* Turned on η-equality for `Record.Record`, removed
+  `Record.Signature′` and `Record.Record′`.
+
+* Renamed `Data.AVL.agda._⊕_sub1` to `pred[_⊕_]`.
diff --git a/CHANGELOG/v0.12.md b/CHANGELOG/v0.12.md
new file mode 100644
index 0000000..d52e776
--- /dev/null
+++ b/CHANGELOG/v0.12.md
@@ -0,0 +1,8 @@
+Version 0.12
+============
+
+The library has been tested using Agda version 2.5.1.
+
+Important changes since 0.11:
+
+* Added support for GHC 8.0.1.
diff --git a/CHANGELOG/v0.13.md b/CHANGELOG/v0.13.md
new file mode 100644
index 0000000..9b75b57
--- /dev/null
+++ b/CHANGELOG/v0.13.md
@@ -0,0 +1,55 @@
+Version 0.13
+============
+
+The library has been tested using Agda version 2.5.2.
+
+Important changes since 0.12:
+
+* Added the `Selective` property in `Algebra.FunctionProperties` as
+  well as proofs of the selectivity of `min` and `max` in
+  `Data.Nat.Properties`.
+
+* Added `Relation.Binary.Product.StrictLex.×-total₂`, an alternative
+  (non-degenerative) proof for totality, and renamed `×-total` to
+  `x-total₁` in that module.
+
+* Added the `length-filter` property to `Data.List.Properties` (the
+  `filter` equivalent to the pre-existing `length-gfilter`).
+
+* Added `_≤?_` decision procedure for `Data.Fin`.
+
+* Added `allPairs` function to `Data.Vec`.
+
+* Added additional properties of `_∈_` to `Data.Vec.Properties`:
+  `∈-map`, `∈-++ₗ`, `∈-++ᵣ`, `∈-allPairs`.
+
+* Added some `zip`/`unzip`-related properties to
+  `Data.Vec.Properties`.
+
+* Added an `All` predicate and related properties for `Data.Vec` (see
+  `Data.Vec.All` and `Data.Vec.All.Properties`).
+
+* Added order-theoretic lattices and some related properties in
+  `Relation.Binary.Lattice` and `Relation.Binary.Properties`.
+
+* Added symmetric and equivalence closures of binary relations in
+  `Relation.Binary.SymmetricClosure` and
+  `Relation.Binary.EquivalenceClosure`.
+
+* Added `Congruent₁` and `Congruent₂` to `Algebra.FunctionProperties`.
+  These are aliases for `_Preserves _≈_ ⟶ _≈_` and
+  `_Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_` from `Relation.Binary.Core`.
+
+* Useful lemmas and properties that were previously in private scope,
+  either explicitly or within records, have been made public in several
+  `Properties.agda` files. These include:
+
+  ```agda
+  Data.Bool.Properties
+
+  Data.Fin.Properties
+
+  Data.Integer.Properties
+  Data.Integer.Addition.Properties
+  Data.Integer.Multiplication.Properties
+  ```
diff --git a/CHANGELOG/v0.14.md b/CHANGELOG/v0.14.md
new file mode 100644
index 0000000..9cd0154
--- /dev/null
+++ b/CHANGELOG/v0.14.md
@@ -0,0 +1,772 @@
+Version 0.14
+============
+
+The library has been tested using Agda version 2.5.3.
+
+Non-backwards compatible changes
+--------------------------------
+
+#### 1st stage of overhaul of list membership
+
+* The current setup for list membership is difficult to work with as both setoid membership
+  and propositional membership exist as internal modules of `Data.Any`. Furthermore the
+  top-level module `Data.List.Any.Membership` actually contains properties of propositional
+  membership rather than the membership relation itself as its name would suggest.
+  Consequently this leaves no place to reason about the properties of setoid membership.
+
+  Therefore the two internal modules `Membership` and `Membership-≡` have been moved out
+  of `Data.List.Any` into top-level `Data.List.Any.Membership` and
+  `Data.List.Any.Membership.Propositional` respectively. The previous module
+  `Data.List.Any.Membership` has been renamed
+  `Data.List.Any.Membership.Propositional.Properties`.
+
+  Accordingly some lemmas have been moved to more logical locations:
+  - `lift-resp` has been moved from `Data.List.Any.Membership` to `Data.List.Any.Properties`
+  - `∈-resp-≈`, `⊆-preorder` and `⊆-Reasoning` have been moved from `Data.List.Any.Membership`
+  to `Data.List.Any.Membership.Properties`.
+  - `∈-resp-list-≈` has been moved from `Data.List.Any.Membership` to
+  `Data.List.Any.Membership.Properties` and renamed `∈-resp-≋`.
+  - `swap` in `Data.List.Any.Properties` has been renamed `swap↔` and made more generic with
+  respect to levels.
+
+#### Moving `decTotalOrder` and `decSetoid` from `Data.X` to `Data.X.Properties`
+
+* Currently the library does not directly expose proofs of basic properties such as reflexivity,
+  transitivity etc. for `_≤_` in numeric datatypes such as `Nat`, `Integer` etc. In order to use these
+  properties it was necessary to first import the `decTotalOrder` proof from `Data.X` and then
+  separately open it, often having to rename the proofs as well. This adds unneccessary lines of
+  code to the import statements for what are very commonly used properties.
+
+  These basic proofs have now been added in `Data.X.Properties` along with proofs that they form
+  pre-orders, partial orders and total orders. This should make them considerably easier to work with
+  and simplify files' import preambles. However consequently the records `decTotalOrder` and
+  `decSetoid` have been moved from `Data.X` to `≤-decTotalOrder` and `≡-decSetoid` in
+  `Data.X.Properties`.
+
+  The numeric datatypes for which this has been done are `Nat`, `Integer`, `Rational` and `Bin`.
+
+  As a consequence the module `≤-Reasoning` has also had to have been moved from `Data.Nat` to
+  `Data.Nat.Properties`.
+
+#### New well-founded induction proofs for `Data.Nat`
+
+* Currently `Induction.Nat` only proves that the non-standard `_<′_`relation over `ℕ` is
+  well-founded. Unfortunately these existing proofs are named `<-Rec` and `<-well-founded`
+  which clash with the sensible names for new proofs over the standard `_<_` relation.
+
+  Therefore `<-Rec` and `<-well-founded` have been renamed to `<′-Rec` and `<′-well-founded`
+  respectively. The original names `<-Rec` and `<-well-founded` now refer to new
+  corresponding proofs for `_<_`.
+
+#### Other
+
+* Changed the implementation of `map` and `zipWith` in `Data.Vec` to use native
+  (pattern-matching) definitions. Previously they were defined using the
+  `applicative` operations of `Vec`. The new definitions can be converted back
+  to the old using the new proofs `⊛-is-zipWith`, `map-is-⊛` and `zipWith-is-⊛`
+  in `Data.Vec.Properties`. It has been argued that `zipWith` is fundamental than `_⊛_`
+  and this change allows better printing of goals involving `map` or `zipWith`.
+
+* Changed the implementation of `All₂` in `Data.Vec.All` to a native datatype. This
+  improved improves pattern matching on terms and allows the new datatype to be more
+  generic with respect to types and levels.
+
+* Changed the implementation of `downFrom` in `Data.List` to a native
+  (pattern-matching) definition. Previously it was defined using a private
+  internal module which made pattern matching difficult.
+
+* The arguments of `≤pred⇒≤` and `≤⇒pred≤` in `Data.Nat.Properties` are now implicit
+  rather than explicit (was `∀ m n → m ≤ pred n → m ≤ n` and is now
+  `∀ {m n} → m ≤ pred n → m ≤ n`). This makes it consistent with `<⇒≤pred` which
+  already used implicit arguments, and shouldn't introduce any significant problems
+  as both parameters can be inferred by Agda.
+
+* Moved `¬∀⟶∃¬` from `Relation.Nullary.Negation` to `Data.Fin.Dec`. Its old
+  location was causing dependency cyles to form between `Data.Fin.Dec`,
+  `Relation.Nullary.Negation` and `Data.Fin`.
+
+* Moved `fold`, `add` and `mul` from `Data.Nat` to new module `Data.Nat.GeneralisedArithmetic`.
+
+* Changed type of second parameter of `Relation.Binary.StrictPartialOrderReasoning._<⟨_⟩_`
+  from `x < y ⊎ x ≈ y` to `x < y`. `_≈⟨_⟩_` is left unchanged to take a value with type `x ≈ y`.
+  Old code may be fixed by prefixing the contents of `_<⟨_⟩_` with `inj₁`.
+
+Deprecated features
+-------------------
+
+Deprecated features still exist and therefore existing code should still work
+but they may be removed in some future release of the library.
+
+* The module `Data.Nat.Properties.Simple` is now deprecated. All proofs
+  have been moved to `Data.Nat.Properties` where they should be used directly.
+  The `Simple` file still exists for backwards compatability reasons and
+  re-exports the proofs from `Data.Nat.Properties` but will be removed in some
+  future release.
+
+* The modules `Data.Integer.Addition.Properties` and
+  `Data.Integer.Multiplication.Properties` are now deprecated. All proofs
+  have been moved to `Data.Integer.Properties` where they should be used
+  directly. The `Addition.Properties` and `Multiplication.Properties` files
+  still exist for backwards compatability reasons and re-exports the proofs from
+  `Data.Integer.Properties` but will be removed in some future release.
+
+* The following renaming has occured in `Data.Nat.Properties`
+  ```agda
+  _+-mono_          ↦  +-mono-≤
+  _*-mono_          ↦  *-mono-≤
+
+  +-right-identity  ↦  +-identityʳ
+  *-right-zero      ↦  *-zeroʳ
+  distribʳ-*-+      ↦  *-distribʳ-+
+  *-distrib-∸ʳ      ↦  *-distribʳ-∸
+  cancel-+-left     ↦  +-cancelˡ-≡
+  cancel-+-left-≤   ↦  +-cancelˡ-≤
+  cancel-*-right    ↦  *-cancelʳ-≡
+  cancel-*-right-≤  ↦  *-cancelʳ-≤
+
+  strictTotalOrder                      ↦  <-strictTotalOrder
+  isCommutativeSemiring                 ↦  *-+-isCommutativeSemiring
+  commutativeSemiring                   ↦  *-+-commutativeSemiring
+  isDistributiveLattice                 ↦  ⊓-⊔-isDistributiveLattice
+  distributiveLattice                   ↦  ⊓-⊔-distributiveLattice
+  ⊔-⊓-0-isSemiringWithoutOne            ↦  ⊔-⊓-isSemiringWithoutOne
+  ⊔-⊓-0-isCommutativeSemiringWithoutOne ↦  ⊔-⊓-isCommutativeSemiringWithoutOne
+  ⊔-⊓-0-commutativeSemiringWithoutOne   ↦  ⊔-⊓-commutativeSemiringWithoutOne
+  ```
+
+* The following renaming has occurred in `Data.Nat.Divisibility`:
+  ```agda
+  ∣-*   ↦   n|m*n
+  ∣-+   ↦   ∣m∣n⇒∣m+n
+  ∣-∸   ↦   ∣m+n|m⇒|n
+  ```
+
+Backwards compatible changes
+----------------------------
+
+* Added support for GHC 8.0.2 and 8.2.1.
+
+* Removed the empty `Irrelevance` module
+
+* Added `Category.Functor.Morphism` and module `Category.Functor.Identity`.
+
+* `Data.Container` and `Data.Container.Indexed` now allow for different
+  levels in the container and in the data it contains.
+
+* Made `Data.BoundedVec` polymorphic with respect to levels.
+
+* Access to `primForce` and `primForceLemma` has been provided via the new
+  top-level module `Strict`.
+
+* New call-by-value application combinator `_$!_` in `Function`.
+
+* Added properties to `Algebra.FunctionProperties`:
+  ```agda
+  LeftCancellative  _•_ = ∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z
+  RightCancellative _•_ = ∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z
+  Cancellative      _•_ = LeftCancellative _•_ × RightCancellative _•_
+  ```
+
+* Added new module `Algebra.FunctionProperties.Consequences` for basic causal relationships between
+  properties, containing:
+  ```agda
+  comm+idˡ⇒idʳ         : Commutative _•_ → LeftIdentity e _•_ → RightIdentity e _•_
+  comm+idʳ⇒idˡ         : Commutative _•_ → RightIdentity e _•_ → LeftIdentity e _•_
+  comm+zeˡ⇒zeʳ         : Commutative _•_ → LeftZero e _•_ → RightZero e _•_
+  comm+zeʳ⇒zeˡ         : Commutative _•_ → RightZero e _•_ → LeftZero e _•_
+  comm+invˡ⇒invʳ       : Commutative _•_ → LeftInverse e _⁻¹ _•_ → RightInverse e _⁻¹ _•_
+  comm+invʳ⇒invˡ       : Commutative _•_ → RightInverse e _⁻¹ _•_ → LeftInverse e _⁻¹ _•_
+  comm+distrˡ⇒distrʳ   : Commutative _•_ → _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_
+  comm+distrʳ⇒distrˡ   : Commutative _•_ → _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_
+  comm+cancelˡ⇒cancelʳ : Commutative _•_ → LeftCancellative _•_ → RightCancellative _•_
+  comm+cancelˡ⇒cancelʳ : Commutative _•_ → LeftCancellative _•_ → RightCancellative _•_
+  sel⇒idem           : Selective _•_ → Idempotent _•_
+  ```
+
+* Added proofs to `Algebra.Properties.BooleanAlgebra`:
+  ```agda
+  ∨-complementˡ : LeftInverse ⊤ ¬_ _∨_
+  ∧-complementˡ : LeftInverse ⊥ ¬_ _∧_
+
+  ∧-identityʳ   : RightIdentity ⊤ _∧_
+  ∧-identityˡ   : LeftIdentity ⊤ _∧_
+  ∧-identity    : Identity ⊤ _∧_
+
+  ∨-identityʳ   : RightIdentity ⊥ _∨_
+  ∨-identityˡ   : LeftIdentity ⊥ _∨_
+  ∨-identity    : Identity ⊥ _∨_
+
+  ∧-zeroʳ       : RightZero ⊥ _∧_
+  ∧-zeroˡ       : LeftZero ⊥ _∧_
+  ∧-zero        : Zero ⊥ _∧_
+
+  ∨-zeroʳ       : RightZero ⊤ _∨_
+  ∨-zeroˡ       : LeftZero ⊤ _∨_
+  ∨-zero        : Zero ⊤ _∨_
+
+  ⊕-identityˡ   : LeftIdentity ⊥ _⊕_
+  ⊕-identityʳ   : RightIdentity ⊥ _⊕_
+  ⊕-identity    : Identity ⊥ _⊕_
+
+  ⊕-inverseˡ    : LeftInverse ⊥ id _⊕_
+  ⊕-inverseʳ    : RightInverse ⊥ id _⊕_
+  ⊕-inverse     : Inverse ⊥ id _⊕_
+
+  ⊕-cong        : Congruent₂ _⊕_
+  ⊕-comm        : Commutative _⊕_
+  ⊕-assoc       : Associative _⊕_
+
+  ∧-distribˡ-⊕  : _∧_ DistributesOverˡ _⊕_
+  ∧-distribʳ-⊕  : _∧_ DistributesOverʳ _⊕_
+  ∧-distrib-⊕   : _∧_ DistributesOver _⊕_
+
+  ∨-isSemigroup           : IsSemigroup _≈_ _∨_
+  ∧-isSemigroup           : IsSemigroup _≈_ _∧_
+  ∨-⊥-isMonoid            : IsMonoid _≈_ _∨_ ⊥
+  ∧-⊤-isMonoid            : IsMonoid _≈_ _∧_ ⊤
+  ∨-⊥-isCommutativeMonoid : IsCommutativeMonoid _≈_ _∨_ ⊥
+  ∧-⊤-isCommutativeMonoid : IsCommutativeMonoid _≈_ _∧_ ⊤
+
+  ⊕-isSemigroup           : IsSemigroup _≈_ _⊕_
+  ⊕-⊥-isMonoid            : IsMonoid _≈_ _⊕_ ⊥
+  ⊕-⊥-isGroup             : IsGroup _≈_ _⊕_ ⊥ id
+  ⊕-⊥-isAbelianGroup      : IsAbelianGroup _≈_ _⊕_ ⊥ id
+  ⊕-∧-isRing              : IsRing _≈_ _⊕_ _∧_ id ⊥ ⊤
+  ```
+
+* Added proofs to `Algebra.Properties.DistributiveLattice`:
+  ```agda
+  ∨-∧-distribˡ : _∨_ DistributesOverˡ _∧_
+  ∧-∨-distribˡ : _∧_ DistributesOverˡ _∨_
+  ∧-∨-distribʳ : _∧_ DistributesOverʳ _∨_
+  ```
+
+* Added pattern synonyms to `Data.Bin` to improve readability:
+  ```agda
+  pattern 0b = zero
+  pattern 1b = 1+ zero
+  pattern ⊥b = 1+ 1+ ()
+  ```
+
+* A new module `Data.Bin.Properties` has been added, containing proofs:
+  ```agda
+  1#-injective         : as 1# ≡ bs 1# → as ≡ bs
+  _≟_                  : Decidable {A = Bin} _≡_
+  ≡-isDecEquivalence   : IsDecEquivalence _≡_
+  ≡-decSetoid          : DecSetoid _ _
+
+  <-trans              : Transitive _<_
+  <-asym               : Asymmetric _<_
+  <-irrefl             : Irreflexive _≡_ _<_
+  <-cmp                : Trichotomous _≡_ _<_
+  <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
+
+  <⇒≢                  : a < b → a ≢ b
+  1<[23]               : [] 1# < (b ∷ []) 1#
+  1<2+                 : [] 1# < (b ∷ bs) 1#
+  0<1+                 : 0# < bs 1#
+  ```
+
+* Added functions to `Data.BoundedVec`:
+  ```agda
+  toInefficient   : BoundedVec A n → Ineff.BoundedVec A n
+  fromInefficient : Ineff.BoundedVec A n → BoundedVec A n
+  ```
+
+* Added the following to `Data.Digit`:
+  ```agda
+  Expansion : ℕ → Set
+  Expansion base = List (Fin base)
+  ```
+
+* Added new module `Data.Empty.Irrelevant` containing an irrelevant version of `⊥-elim`.
+
+* Added functions to `Data.Fin`:
+  ```agda
+  punchIn  i j ≈ if j≥i then j+1 else j
+  punchOut i j ≈ if j>i then j-1 else j
+  ```
+
+* Added proofs to `Data.Fin.Properties`:
+  ```agda
+  isDecEquivalence     : ∀ {n} → IsDecEquivalence (_≡_ {A = Fin n})
+
+  ≤-reflexive          : ∀ {n} → _≡_ ⇒ (_≤_ {n})
+  ≤-refl               : ∀ {n} → Reflexive (_≤_ {n})
+  ≤-trans              : ∀ {n} → Transitive (_≤_ {n})
+  ≤-antisymmetric      : ∀ {n} → Antisymmetric _≡_ (_≤_ {n})
+  ≤-total              : ∀ {n} → Total (_≤_ {n})
+  ≤-isPreorder         : ∀ {n} → IsPreorder _≡_ (_≤_ {n})
+  ≤-isPartialOrder     : ∀ {n} → IsPartialOrder _≡_ (_≤_ {n})
+  ≤-isTotalOrder       : ∀ {n} → IsTotalOrder _≡_ (_≤_ {n})
+
+  _<?_                 : ∀ {n} → Decidable (_<_ {n})
+  <-trans              : ∀ {n} → Transitive (_<_ {n})
+  <-isStrictTotalOrder : ∀ {n} → IsStrictTotalOrder _≡_ (_<_ {n})
+
+  punchOut-injective   : punchOut i≢j ≡ punchOut i≢k → j ≡ k
+  punchIn-injective    : punchIn i j ≡ punchIn i k → j ≡ k
+  punchIn-punchOut     : punchIn i (punchOut i≢j) ≡ j
+  punchInᵢ≢i           : punchIn i j ≢ i
+  ```
+
+* Added proofs to `Data.Fin.Subset.Properties`:
+  ```agda
+  x∈⁅x⁆     : x ∈ ⁅ x ⁆
+  x∈⁅y⁆⇒x≡y : x ∈ ⁅ y ⁆ → x ≡ y
+
+  ∪-assoc   : Associative _≡_ _∪_
+  ∩-assoc   : Associative _≡_ _∩_
+  ∪-comm    : Commutative _≡_ _∪_
+  ∩-comm    : Commutative _≡_ _∩_
+
+  p⊆p∪q     : p ⊆ p ∪ q
+  q⊆p∪q     : q ⊆ p ∪ q
+  x∈p∪q⁻    : x ∈ p ∪ q → x ∈ p ⊎ x ∈ q
+  x∈p∪q⁺    : x ∈ p ⊎ x ∈ q → x ∈ p ∪ q
+
+  p∩q⊆p     : p ∩ q ⊆ p
+  p∩q⊆q     : p ∩ q ⊆ q
+  x∈p∩q⁺    : x ∈ p × x ∈ q → x ∈ p ∩ q
+  x∈p∩q⁻    : x ∈ p ∩ q → x ∈ p × x ∈ q
+  ∩⇔×       : x ∈ p ∩ q ⇔ (x ∈ p × x ∈ q)
+  ```
+
+* Added relations to `Data.Integer`
+  ```agda
+  _≥_ : Rel ℤ _
+  _<_ : Rel ℤ _
+  _>_ : Rel ℤ _
+  _≰_ : Rel ℤ _
+  _≱_ : Rel ℤ _
+  _≮_ : Rel ℤ _
+  _≯_ : Rel ℤ _
+  ```
+
+* Added proofs to `Data.Integer.Properties`
+  ```agda
+  +-injective           : + m ≡ + n → m ≡ n
+  -[1+-injective        : -[1+ m ] ≡ -[1+ n ] → m ≡ n
+
+  doubleNeg             : - - n ≡ n
+  neg-injective         : - m ≡ - n → m ≡ n
+
+  ∣n∣≡0⇒n≡0             : ∣ n ∣ ≡ 0 → n ≡ + 0
+  ∣-n∣≡∣n∣              : ∣ - n ∣ ≡ ∣ n ∣
+
+  +◃n≡+n                : Sign.+ ◃ n ≡ + n
+  -◃n≡-n                : Sign.- ◃ n ≡ - + n
+  signₙ◃∣n∣≡n           : sign n ◃ ∣ n ∣ ≡ n
+  ∣s◃m∣*∣t◃n∣≡m*n       : ∣ s ◃ m ∣ ℕ* ∣ t ◃ n ∣ ≡ m ℕ* n
+
+  ⊖-≰                   : n ≰ m → m ⊖ n ≡ - + (n ∸ m)
+  ∣⊖∣-≰                 : n ≰ m → ∣ m ⊖ n ∣ ≡ n ∸ m
+  sign-⊖-≰              : n ≰ m → sign (m ⊖ n) ≡ Sign.-
+  -[n⊖m]≡-m+n           : - (m ⊖ n) ≡ (- (+ m)) + (+ n)
+
+  +-identity            : Identity (+ 0) _+_
+  +-inverse             : Inverse (+ 0) -_ _+_
+  +-0-isMonoid          : IsMonoid _≡_ _+_ (+ 0)
+  +-0-isGroup           : IsGroup _≡_ _+_ (+ 0) (-_)
+  +-0-abelianGroup      : AbelianGroup _ _
+
+  n≢1+n                 : n ≢ suc n
+  1-[1+n]≡-n            : suc -[1+ n ] ≡ - (+ n)
+  neg-distrib-+         : - (m + n) ≡ (- m) + (- n)
+  ◃-distrib-+           : s ◃ (m + n) ≡ (s ◃ m) + (s ◃ n)
+
+  *-identityʳ           : RightIdentity (+ 1) _*_
+  *-identity            : Identity (+ 1) _*_
+  *-zeroˡ               : LeftZero (+ 0) _*_
+  *-zeroʳ               : RightZero (+ 0) _*_
+  *-zero                : Zero (+ 0) _*_
+  *-1-isMonoid          : IsMonoid _≡_ _*_ (+ 1)
+  -1*n≡-n               : -[1+ 0 ] * n ≡ - n
+  ◃-distrib-*           : (s 𝕊* t) ◃ (m ℕ* n) ≡ (s ◃ m) * (t ◃ n)
+
+  +-*-isRing            : IsRing _≡_ _+_ _*_ -_ (+ 0) (+ 1)
+  +-*-isCommutativeRing : IsCommutativeRing _≡_ _+_ _*_ -_ (+ 0) (+ 1)
+
+  ≤-reflexive           : _≡_ ⇒ _≤_
+  ≤-refl                : Reflexive _≤_
+  ≤-trans               : Transitive _≤_
+  ≤-antisym             : Antisymmetric _≡_ _≤_
+  ≤-total               : Total _≤_
+
+  ≤-isPreorder          : IsPreorder _≡_ _≤_
+  ≤-isPartialOrder      : IsPartialOrder _≡_ _≤_
+  ≤-isTotalOrder        : IsTotalOrder _≡_ _≤_
+  ≤-isDecTotalOrder     : IsDecTotalOrder _≡_ _≤_
+
+  ≤-step                : n ≤ m → n ≤ suc m
+  n≤1+n                 : n ≤ + 1 + n
+
+  <-irrefl              : Irreflexive _≡_ _<_
+  <-asym                : Asymmetric _<_
+  <-trans               : Transitive _<_
+  <-cmp                 : Trichotomous _≡_ _<_
+  <-isStrictTotalOrder  : IsStrictTotalOrder _≡_ _<_
+
+  n≮n                   : n ≮ n
+  -<+                   : -[1+ m ] < + n
+  <⇒≤                   : m < n → m ≤ n
+  ≰→>                   : x ≰ y → x > y
+  ```
+
+* Added functions to `Data.List`
+  ```agda
+  applyUpTo f n     ≈ f[0]   ∷ f[1]   ∷ ... ∷ f[n-1] ∷ []
+  upTo n            ≈ 0      ∷ 1      ∷ ... ∷ n-1    ∷ []
+  applyDownFrom f n ≈ f[n-1] ∷ f[n-2] ∷ ... ∷ f[0]   ∷ []
+  tabulate f        ≈ f[0]   ∷ f[1]   ∷ ... ∷ f[n-1] ∷ []
+  allFin n          ≈ 0f     ∷ 1f     ∷ ... ∷ n-1f   ∷ []
+  ```
+
+* Added proofs to `Data.List.Properties`
+  ```agda
+  map-id₂        : All (λ x → f x ≡ x) xs → map f xs ≡ xs
+  map-cong₂      : All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs
+  foldr-++       : foldr f x (ys ++ zs) ≡ foldr f (foldr f x zs) ys
+  foldl-++       : foldl f x (ys ++ zs) ≡ foldl f (foldl f x ys) zs
+  foldr-∷ʳ       : foldr f x (ys ∷ʳ y) ≡ foldr f (f y x) ys
+  foldl-∷ʳ       : foldl f x (ys ∷ʳ y) ≡ f (foldl f x ys) y
+  reverse-foldr  : foldr f x (reverse ys) ≡ foldl (flip f) x ys
+  reverse-foldr  : foldl f x (reverse ys) ≡ foldr (flip f) x ys
+  length-reverse : length (reverse xs) ≡ length xs
+  ```
+
+* Added proofs to `Data.List.All.Properties`
+  ```agda
+  All-universal : Universal P → All P xs
+
+  ¬Any⇒All¬     : ¬ Any P xs → All (¬_ ∘ P) xs
+  All¬⇒¬Any     : All (¬_ ∘ P) xs → ¬ Any P xs
+  ¬All⇒Any¬     : Decidable P → ¬ All P xs → Any (¬_ ∘ P) xs
+
+  ++⁺           : All P xs → All P ys → All P (xs ++ ys)
+  ++⁻ˡ          : All P (xs ++ ys) → All P xs
+  ++⁻ʳ          : All P (xs ++ ys) → All P ys
+  ++⁻           : All P (xs ++ ys) → All P xs × All P ys
+
+  concat⁺       : All (All P) xss → All P (concat xss)
+  concat⁻       : All P (concat xss) → All (All P) xss
+
+  drop⁺         : All P xs → All P (drop n xs)
+  take⁺         : All P xs → All P (take n xs)
+
+  tabulate⁺     : (∀ i → P (f i)) → All P (tabulate f)
+  tabulate⁻     : All P (tabulate f) → (∀ i → P (f i))
+
+  applyUpTo⁺₁   : (∀ {i} → i < n → P (f i)) → All P (applyUpTo f n)
+  applyUpTo⁺₂   : (∀ i → P (f i)) → All P (applyUpTo f n)
+  applyUpTo⁻    : All P (applyUpTo f n) → ∀ {i} → i < n → P (f i)
+  ```
+
+* Added proofs to `Data.List.Any.Properties`
+  ```agda
+  lose∘find   : uncurry′ lose (proj₂ (find p)) ≡ p
+  find∘lose   : find (lose x∈xs pp) ≡ (x , x∈xs , pp)
+
+  swap        : Any (λ x → Any (P x) ys) xs → Any (λ y → Any (flip P y) xs) ys
+  swap-invol  : swap (swap any) ≡ any
+
+  ∃∈-Any      : (∃ λ x → x ∈ xs × P x) → Any P xs
+
+  Any-⊎⁺      : Any P xs ⊎ Any Q xs → Any (λ x → P x ⊎ Q x) xs
+  Any-⊎⁻      : Any (λ x → P x ⊎ Q x) xs → Any P xs ⊎ Any Q xs
+  Any-×⁺      : Any P xs × Any Q ys → Any (λ x → Any (λ y → P x × Q y) ys) xs
+  Any-×⁻      : Any (λ x → Any (λ y → P x × Q y) ys) xs → Any P xs × Any Q ys
+
+  map⁺        : Any (P ∘ f) xs → Any P (map f xs)
+  map⁻        : Any P (map f xs) → Any (P ∘ f) xs
+
+  ++⁺ˡ        : Any P xs → Any P (xs ++ ys)
+  ++⁺ʳ        : Any P ys → Any P (xs ++ ys)
+  ++⁻         : Any P (xs ++ ys) → Any P xs ⊎ Any P ys
+
+  concat⁺     : Any (Any P) xss → Any P (concat xss)
+  concat⁻     : Any P (concat xss) → Any (Any P) xss
+
+  applyUpTo⁺  : P (f i) → i < n → Any P (applyUpTo f n)
+  applyUpTo⁻  : Any P (applyUpTo f n) → ∃ λ i → i < n × P (f i)
+
+  tabulate⁺   : P (f i) → Any P (tabulate f)
+  tabulate⁻   : Any P (tabulate f) → ∃ λ i → P (f i)
+
+  map-with-∈⁺ : (∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) → Any P (map-with-∈ xs f)
+  map-with-∈⁻ : Any P (map-with-∈ xs f) → ∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)
+
+  return⁺     : P x → Any P (return x)
+  return⁻     : Any P (return x) → P x
+  ```
+
+* Added proofs to `Data.List.Any.Membership.Properties`
+  ```agda
+  ∈-map⁺ :  x ∈ xs → f x ∈ map f xs
+  ∈-map⁻ :  y ∈ map f xs → ∃ λ x → x ∈ xs × y ≈ f x
+  ```
+
+* Added proofs to `Data.List.Any.Membership.Propositional.Properties`
+  ```agda
+  ∈-map⁺ :  x ∈ xs → f x ∈ map f xs
+  ∈-map⁻ :  y ∈ map f xs → ∃ λ x → x ∈ xs × y ≈ f x
+  ```
+
+* Added proofs to `Data.Maybe`:
+  ```agda
+  Eq-refl             : Reflexive _≈_ → Reflexive (Eq _≈_)
+  Eq-sym              : Symmetric _≈_ → Symmetric (Eq _≈_)
+  Eq-trans            : Transitive _≈_ → Transitive (Eq _≈_)
+  Eq-dec              : Decidable _≈_ → Decidable (Eq _≈_)
+  Eq-isEquivalence    : IsEquivalence _≈_ → IsEquivalence (Eq _≈_)
+  Eq-isDecEquivalence : IsDecEquivalence _≈_ → IsDecEquivalence (Eq _≈_)
+  ```
+
+* Added exponentiation operator `_^_` to `Data.Nat.Base`
+
+* Added proofs to `Data.Nat.Properties`:
+  ```agda
+  suc-injective         : suc m ≡ suc n → m ≡ n
+  ≡-isDecEquivalence    : IsDecEquivalence (_≡_ {A = ℕ})
+  ≡-decSetoid           : DecSetoid _ _
+
+  ≤-reflexive           : _≡_ ⇒ _≤_
+  ≤-refl                : Reflexive _≤_
+  ≤-trans               : Antisymmetric _≡_ _≤_
+  ≤-antisymmetric       : Transitive _≤_
+  ≤-total               : Total _≤_
+  ≤-isPreorder          : IsPreorder _≡_ _≤_
+  ≤-isPartialOrder      : IsPartialOrder _≡_ _≤_
+  ≤-isTotalOrder        : IsTotalOrder _≡_ _≤_
+  ≤-isDecTotalOrder     : IsDecTotalOrder _≡_ _≤_
+
+  _<?_                  : Decidable _<_
+  <-irrefl              : Irreflexive _≡_ _<_
+  <-asym                : Asymmetric _<_
+  <-transʳ              : Trans _≤_ _<_ _<_
+  <-transˡ              : Trans _<_ _≤_ _<_
+  <-isStrictTotalOrder  : IsStrictTotalOrder _≡_ _<_
+  <⇒≤                   : _<_ ⇒ _≤_
+  <⇒≢                   : _<_ ⇒ _≢_
+  <⇒≱                   : _<_ ⇒ _≱_
+  <⇒≯                   : _<_ ⇒ _≯_
+  ≰⇒≮                   : _≰_ ⇒ _≮_
+  ≰⇒≥                   : _≰_ ⇒ _≥_
+  ≮⇒≥                   : _≮_ ⇒ _≥_
+  ≤+≢⇒<                 : m ≤ n → m ≢ n → m < n
+
+  +-identityˡ           : LeftIdentity 0 _+_
+  +-identity            : Identity 0 _+_
+  +-cancelʳ-≡           : RightCancellative _≡_ _+_
+  +-cancel-≡            : Cancellative _≡_ _+_
+  +-cancelʳ-≤           : RightCancellative _≤_ _+_
+  +-cancel-≤            : Cancellative _≤_ _+_
+  +-isSemigroup         : IsSemigroup _≡_ _+_
+  +-monoˡ-<             : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
+  +-monoʳ-<             : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
+  +-mono-<              : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+  m+n≤o⇒m≤o             : m + n ≤ o → m ≤ o
+  m+n≤o⇒n≤o             : m + n ≤ o → n ≤ o
+  m+n≮n                 : m + n ≮ n
+
+  *-zeroˡ               : LeftZero 0 _*_
+  *-zero                : Zero 0 _*_
+  *-identityˡ           : LeftIdentity 1 _*_
+  *-identityʳ           : RightIdentity 1 _*_
+  *-identity            : Identity 1 _*_
+  *-distribˡ-+          : _*_ DistributesOverˡ _+_
+  *-distrib-+           : _*_ DistributesOver _+_
+  *-isSemigroup         : IsSemigroup _≡_ _*_
+  *-mono-<              : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+  *-monoˡ-<             : (_* suc n) Preserves _<_ ⟶ _<_
+  *-monoʳ-<             : (suc n *_) Preserves _<_ ⟶ _<_
+  *-cancelˡ-≡           : suc k * i ≡ suc k * j → i ≡ j
+
+  ^-distribˡ-+-*        : m ^ (n + p) ≡ m ^ n * m ^ p
+  i^j≡0⇒i≡0             : i ^ j ≡ 0 → i ≡ 0
+  i^j≡1⇒j≡0∨i≡1         : i ^ j ≡ 1 → j ≡ 0 ⊎ i ≡ 1
+
+  ⊔-assoc               : Associative _⊔_
+  ⊔-comm                : Commutative _⊔_
+  ⊔-idem                : Idempotent _⊔_
+  ⊔-identityˡ           : LeftIdentity 0 _⊔_
+  ⊔-identityʳ           : RightIdentity 0 _⊔_
+  ⊔-identity            : Identity 0 _⊔_
+  ⊓-assoc               : Associative _⊓_
+  ⊓-comm                : Commutative _⊓_
+  ⊓-idem                : Idempotent _⊓_
+  ⊓-zeroˡ               : LeftZero 0 _⊓_
+  ⊓-zeroʳ               : RightZero 0 _⊓_
+  ⊓-zero                : Zero 0 _⊓_
+  ⊓-distribʳ-⊔          : _⊓_ DistributesOverʳ _⊔_
+  ⊓-distribˡ-⊔          : _⊓_ DistributesOverˡ _⊔_
+  ⊔-abs-⊓               : _⊔_ Absorbs _⊓_
+  ⊓-abs-⊔               : _⊓_ Absorbs _⊔_
+  m⊓n≤n                 : m ⊓ n ≤ n
+  m≤m⊔n                 : m ≤ m ⊔ n
+  m⊔n≤m+n               : m ⊔ n ≤ m + n
+  m⊓n≤m+n               : m ⊓ n ≤ m + n
+  m⊓n≤m⊔n               : m ⊔ n ≤ m ⊔ n
+  ⊔-mono-≤              : _⊔_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
+  ⊔-mono-<              : _⊔_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+  ⊓-mono-≤              : _⊓_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
+  ⊓-mono-<              : _⊓_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+  +-distribˡ-⊔          : _+_ DistributesOverˡ _⊔_
+  +-distribʳ-⊔          : _+_ DistributesOverʳ _⊔_
+  +-distrib-⊔           : _+_ DistributesOver _⊔_
+  +-distribˡ-⊓          : _+_ DistributesOverˡ _⊓_
+  +-distribʳ-⊓          : _+_ DistributesOverʳ _⊓_
+  +-distrib-⊓           : _+_ DistributesOver _⊓_
+  ⊔-isSemigroup         : IsSemigroup _≡_ _⊔_
+  ⊓-isSemigroup         : IsSemigroup _≡_ _⊓_
+  ⊓-⊔-isLattice         : IsLattice _≡_ _⊓_ _⊔_
+
+  ∸-distribʳ-⊔          : _∸_ DistributesOverʳ _⊔_
+  ∸-distribʳ-⊓          : _∸_ DistributesOverʳ _⊓_
+  +-∸-comm              : o ≤ m → (m + n) ∸ o ≡ (m ∸ o) + n
+  ```
+
+* Added decidability relation to `Data.Nat.GCD`
+  ```agda
+  gcd? : (m n d : ℕ) → Dec (GCD m n d)
+  ```
+
+* Added "not-divisible-by" relation to `Data.Nat.Divisibility`
+  ```agda
+  m ∤ n = ¬ (m ∣ n)
+  ```
+
+* Added proofs to `Data.Nat.Divisibility`
+  ```agda
+  ∣-reflexive      : _≡_ ⇒ _∣_
+  ∣-refl           : Reflexive _∣_
+  ∣-trans          : Transitive _∣_
+  ∣-antisym        : Antisymmetric _≡_ _∣_
+  ∣-isPreorder     : IsPreorder _≡_ _∣_
+  ∣-isPartialOrder : IsPartialOrder _≡_ _∣_
+
+  n∣n              : n ∣ n
+  ∣m∸n∣n⇒∣m        : n ≤ m → i ∣ m ∸ n → i ∣ n → i ∣ m
+  ```
+
+* Added proofs to `Data.Nat.GeneralisedArithmetic`:
+  ```agda
+  fold-+     : fold z s (m + n) ≡ fold (fold z s n) s m
+  fold-k     : fold k (s ∘′_) m z ≡ fold (k z) s m
+  fold-*     : fold z s (m * n) ≡ fold z (fold id (s ∘_) n) m
+  fold-pull  : fold p s m ≡ g (fold z s m) p
+
+  id-is-fold : fold zero suc m ≡ m
+  +-is-fold  : fold n suc m ≡ m + n
+  *-is-fold  : fold zero (n +_) m ≡ m * n
+  ^-is-fold  : fold 1 (m *_) n ≡ m ^ n
+  *+-is-fold : fold p (n +_) m ≡ m * n + p
+  ^*-is-fold : fold p (m *_) n ≡ m ^ n * p
+  ```
+
+* Added syntax for existential quantifiers in `Data.Product`:
+  ```agda
+  ∃-syntax (λ x → B) = ∃[ x ] B
+  ∄-syntax (λ x → B) = ∄[ x ] B
+  ```
+
+* A new module `Data.Rational.Properties` has been added, containing proofs:
+  ```agda
+  ≤-reflexive : _≡_ ⇒ _≤_
+  ≤-refl      : Reflexive _≤_
+  ≤-trans     : Transitive _≤_
+  ≤-antisym   : Antisymmetric _≡_ _≤_
+  ≤-total     : Total _≤_
+
+  ≤-isPreorder : IsPreorder _≡_ _≤_
+  ≤-isPartialOrder : IsPartialOrder _≡_ _≤_
+  ≤-isTotalOrder : IsTotalOrder _≡_ _≤_
+  ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
+  ```
+
+* Added proofs to `Data.Sign.Properties`:
+  ```agda
+  opposite-cong  : opposite s ≡ opposite t → s ≡ t
+
+  *-identityˡ    : LeftIdentity + _*_
+  *-identityʳ    : RightIdentity + _*_
+  *-identity     : Identity + _*_
+  *-comm         : Commutative _*_
+  *-assoc        : Associative _*_
+  cancel-*-left  : LeftCancellative _*_
+  *-cancellative : Cancellative _*_
+  s*s≡+          : s * s ≡ +
+  ```
+
+* Added definitions to `Data.Sum`:
+  ```agda
+  From-inj₁ : ∀ {a b} {A : Set a} {B : Set b} → A ⊎ B → Set a
+  from-inj₁ : ∀ {a b} {A : Set a} {B : Set b} (x : A ⊎ B) → From-inj₁ x
+  From-inj₂ : ∀ {a b} {A : Set a} {B : Set b} → A ⊎ B → Set b
+  from-inj₂ : ∀ {a b} {A : Set a} {B : Set b} (x : A ⊎ B) → From-inj₂ x
+  ```
+
+* Added a functor encapsulating `map` in `Data.Vec`:
+  ```agda
+  functor = record { _<$>_ = map}
+  ```
+
+* Added proofs to `Data.Vec.Equality`
+  ```agda
+  to-≅      : xs ≈ ys → xs ≅ ys
+  xs++[]≈xs  : xs ++ [] ≈ xs
+  xs++[]≅xs : xs ++ [] ≅ xs
+  ```
+
+* Added proofs to `Data.Vec.Properties`
+  ```agda
+  lookup-map              : lookup i (map f xs) ≡ f (lookup i xs)
+  lookup-functor-morphism : Morphism functor IdentityFunctor
+  map-replicate           : map f (replicate x) ≡ replicate (f x)
+
+  ⊛-is-zipWith            : fs ⊛ xs ≡ zipWith _$_ fs xs
+  map-is-⊛                : map f xs ≡ replicate f ⊛ xs
+  zipWith-is-⊛            : zipWith f xs ys ≡ replicate f ⊛ xs ⊛ ys
+
+  zipWith-replicate₁      : zipWith _⊕_ (replicate x) ys ≡ map (x ⊕_) ys
+  zipWith-replicate₂      : zipWith _⊕_ xs (replicate y) ≡ map (_⊕ y) xs
+  zipWith-map₁            : zipWith _⊕_ (map f xs) ys ≡ zipWith (λ x y → f x ⊕ y) xs ys
+  zipWith-map₂            : zipWith _⊕_ xs (map f ys) ≡ zipWith (λ x y → x ⊕ f y) xs ys
+  ```
+
+* Added proofs to `Data.Vec.All.Properties`
+  ```agda
+  All-++⁺      : All P xs → All P ys → All P (xs ++ ys)
+  All-++ˡ⁻     : All P (xs ++ ys) → All P xs
+  All-++ʳ⁻     : All P (xs ++ ys) → All P ys
+  All-++⁻      : All P (xs ++ ys) → All P xs × All P ys
+
+  All₂-++⁺     : All₂ _~_ ws xs → All₂ _~_ ys zs → All₂ _~_ (ws ++ ys) (xs ++ zs)
+  All₂-++ˡ⁻    : All₂ _~_ (ws ++ ys) (xs ++ zs) → All₂ _~_ ws xs
+  All₂-++ʳ⁻    : All₂ _~_ (ws ++ ys) (xs ++ zs) → All₂ _~_ ys zs
+  All₂-++⁻     : All₂ _~_ (ws ++ ys) (xs ++ zs) → All₂ _~_ ws xs × All₂ _~_ ys zs
+
+  All-concat⁺  : All (All P) xss → All P (concat xss)
+  All-concat⁻  : All P (concat xss) → All (All P) xss
+
+  All₂-concat⁺ : All₂ (All₂ _~_) xss yss → All₂ _~_ (concat xss) (concat yss)
+  All₂-concat⁻ : All₂ _~_ (concat xss) (concat yss) → All₂ (All₂ _~_) xss yss
+  ```
+
+* Added non-dependant versions of the application combinators in `Function` for use
+  cases where the most general one leads to unsolved meta variables:
+  ```agda
+  _$′_  : (A → B) → (A → B)
+  _$!′_ : (A → B) → (A → B)
+  ```
+
+* Added proofs to `Relation.Binary.Consequences`
+  ```agda
+  P-resp⟶¬P-resp : Symmetric _≈_ → P Respects _≈_ → (¬_ ∘ P) Respects _≈_
+  ```
+
+* Added conversion lemmas to `Relation.Binary.HeterogeneousEquality`
+  ```agda
+  ≅-to-type-≡  : {x : A} {y : B} → x ≅ y → A ≡ B
+  ≅-to-subst-≡ : (p : x ≅ y) → subst (λ x → x) (≅-to-type-≡ p) x ≡ y
+  ```
diff --git a/CHANGELOG/v0.15.md b/CHANGELOG/v0.15.md
new file mode 100644
index 0000000..5946964
--- /dev/null
+++ b/CHANGELOG/v0.15.md
@@ -0,0 +1,762 @@
+Version 0.15
+============
+
+The library has been tested using Agda version 2.5.3.
+
+Non-backwards compatible changes
+--------------------------------
+
+#### Upgrade and overhaul of organisation of relations over data
+
+* Relations over data have been moved from the `Relation` subtree to the `Data`
+  subtree. This increases the usability of the library by:
+    1. keeping all the definitions concerning a given datatype in the same directory
+    2. providing a location to reason about how operations on the data affect the
+       relations (e.g. how `Pointwise` is affected by `map`)
+    3. increasing the discoverability of the relations. There is anecdotal evidence that many
+           users were not aware of the existence of the relations in the old location.
+
+  In general the files have been moved from `Relation.Binary.X` to
+  `Data.X.Relation`. The full list of moves is as follows:
+  ```
+  `Relation.Binary.List.Pointwise`       ↦ `Data.List.Relation.Pointwise`
+  `Relation.Binary.List.StrictLex`       ↦ `Data.List.Relation.Lex.Strict`
+  `Relation.Binary.List.NonStrictLex`    ↦ `Data.List.Relation.Lex.NonStrict`
+  `Relation.Binary.Sum`                  ↦ `Data.Sum.Relation.Pointwise`
+                                         ↘ `Data.Sum.Relation.LeftOrder`
+  `Relation.Binary.Sigma.Pointwise`      ↦ `Data.Product.Relation.Pointwise.Dependent'
+  `Relation.Binary.Product.Pointwise`    ↦ `Data.Product.Relation.Pointwise.NonDependent`
+  `Relation.Binary.Product.StrictLex`    ↦ `Data.Product.Relation.Lex.Strict`
+  `Relation.Binary.Product.NonStrictLex` ↦ `Data.Product.Relation.Lex.NonStrict`
+  `Relation.Binary.Vec.Pointwise`        ↦ `Data.Vec.Relation.Pointwise.Inductive`
+                                         ↘ `Data.Vec.Relation.Pointwise.Extensional`
+  ```
+
+  The old files in `Relation.Binary.X` still exist for backwards compatability reasons and
+  re-export the contents of files' new location in `Data.X.Relation` but may be removed in some
+  future release.
+
+* The contents of `Relation.Binary.Sum` has been split into two modules
+  `Data.Sum.Relation.Pointwise` and `Data.Sum.Relation.LeftOrder`
+
+* The contents of `Relation.Binary.Vec.Pointwise` has been split into two modules
+  `Data.Vec.Relation.Pointwise.Inductive` and `Data.Vec.Relation.Pointwise.Extensional`.
+
+  The inductive form of `Pointwise` has been generalised so that technically it can apply to two
+  vectors with different lengths (although in practice the lengths must turn out to be equal). This
+  allows a much wider range of proofs such as the fact that `[]` is a right identity for `_++_`
+  which previously did not type check using the old definition. In order to ensure
+  compatability with the `--without-K` option, the universe level of `Inductive.Pointwise`
+  has been increased from `ℓ` to `a ⊔ b ⊔ ℓ`.
+
+* `Data.Vec.Equality` has been almost entirely reworked into four separate modules
+  inside `Data.Vec.Relation.Equality` (namely `Setoid`, `DecSetoid`, `Propositional`
+  and `DecPropositional`). All four of them now use `Data.Vec.Relation.Pointwise.Inductive`
+  as a base.
+
+  The proofs from the submodule `UsingVecEquality` in `Data.Vec.Properties` have been moved
+  to these four new modules.
+
+* The datatype `All₂` has been removed from `Data.Vec.All`, along with associated proofs
+  as it duplicates existing functionality in `Data.Vec.Relation.Pointwise.Inductive`.
+  Unfortunately it is not possible to maintain backwards compatability due to dependency
+  cycles.
+
+* Added new modules
+  `Data.List.Relation.Equality.(Setoid/DecSetoid/Propositional/DecPropositional)`.
+
+#### Upgrade of `Data.AVL`
+
+* `Data.AVL.Key` and `Data.AVL.Height` have been split out of `Data.AVL`
+  therefore ensuring they are independent on the type of `Value` the tree contains.
+
+* `Indexed` has been put into its own core module `Data.AVL.Indexed`, following the
+  example of `Category.Monad.Indexed` and `Data.Container.Indexed`.
+
+* These changes allow `map` to have a polymorphic type and so it is now possible
+  to change the type of values contained in a tree when mapping over it.
+
+#### Upgrade of `Algebra.Morphism`
+
+* Previously `Algebra.Morphism` only provides an example of a `Ring` homomorphism which
+  packs the homomorphism and the proofs that it behaves the right way.
+
+  Instead we have adopted and `Algebra.Structures`-like approach with proof-only
+  records parametrised by the homomorphism and the structures it acts on. This make
+  it possible to define the proof requirement for e.g. a ring in terms of the proof
+  requirements for its additive abelian group and multiplicative monoid.
+
+#### Upgrade of `filter` and `partition` in `Data.List`
+
+* The functions `filter` and `partition` in `Data.List.Base` now use decidable
+  predicates instead of boolean-valued functions. The boolean versions discarded
+  type information, and hence were difficult to use and prove
+  properties about. The proofs have been updated and renamed accordingly.
+
+  The old boolean versions still exist as `boolFilter` and `boolPartition` for
+  backwards compatibility reasons, but are deprecated and may be removed in some
+  future release. The old versions can be implemented via the new versions
+  by passing the decidability proof `λ v → f v ≟ true` with `_≟_` from `Data.Bool`.
+
+#### Overhaul of categorical interpretations of List and Vec
+
+* New modules `Data.List.Categorical` and `Data.Vec.Categorical` have been added
+  for the categorical interpretations of `List` and `Vec`.
+
+  The following have been moved to `Data.List.Categorical`:
+
+  - The module `Monad` from `Data.List.Properties` (renamed to `MonadProperties`)
+  - The module `Applicative` from `Data.List.Properties`
+  - `monad`, `monadZero`, `monadPlus` and monadic operators from `Data.List`
+
+  The following has been moved to `Data.Vec.Categorical`:
+
+  - `applicative` and `functor` from `Data.Vec`
+  - `lookup-morphism` and `lookup-functor-morphism` from `Data.Vec.Properties`
+
+#### Other
+
+* Removed support for GHC 7.8.4.
+
+* Renamed `Data.Container.FreeMonad.do` and `Data.Container.Indexed.FreeMonad.do`
+  to `inn` as Agda 2.5.4 now supports proper 'do' notation.
+
+* Changed the fixity of `⋃` and `⋂` in `Relation.Unary` to make space for `_⊢_`.
+
+* Changed `_|_` from `Data.Nat.Divisibility` from data to a record. Consequently,
+  the two parameters are no longer implicit arguments of the constructor (but
+  such values can be destructed using a let-binding rather than a with-clause).
+
+* Names in `Data.Nat.Divisibility` now use the `divides` symbol (typed \\|) consistently.
+  Previously a mixture of \\| and | was used.
+
+* Moved the proof `eq?` from `Data.Nat` to `Data.Nat.Properties`
+
+* The proofs that were called `+-monoˡ-<` and `+-monoʳ-<` in `Data.Nat.Properties`
+  have been renamed `+-mono-<-≤` and `+-mono-≤-<` respectively. The original
+  names are now used for proofs of left and right monotonicity of `_+_`.
+
+* Moved the proof `monoid` from `Data.List` to `++-monoid` in `Data.List.Properties`.
+
+* Names in Data.Nat.Divisibility now use the `divides` symbol (typed \\|) consistently.
+  Previously a mixture of \\| and | was used.
+
+* Starting from Agda 2.5.4 the GHC backend compiles `Coinduction.∞` in
+  a different way, and for this reason the GHC backend pragmas for
+  `Data.Colist.Colist` and `Data.Stream.Stream` have been modified.
+
+Deprecated features
+-------------------
+
+The following renaming has occurred as part of a drive to improve consistency across
+the library. The old names still exist and therefore all existing code should still
+work, however they have been deprecated and use of the new names is encouraged. Although not
+anticipated any time soon, they may eventually be removed in some future release of the library.
+
+* In `Data.Bool.Properties`:
+  ```agda
+  ∧-∨-distˡ      ↦ ∧-distribˡ-∨
+  ∧-∨-distʳ      ↦ ∧-distribʳ-∨
+  distrib-∧-∨    ↦ ∧-distrib-∨
+  ∨-∧-distˡ      ↦ ∨-distribˡ-∧
+  ∨-∧-distʳ      ↦ ∨-distribʳ-∧
+  ∨-∧-distrib    ↦ ∨-distrib-∧
+  ∨-∧-abs        ↦ ∨-abs-∧
+  ∧-∨-abs        ↦ ∧-abs-∨
+
+  not-∧-inverseˡ ↦ ∧-inverseˡ
+  not-∧-inverseʳ ↦ ∧-inverseʳ
+  not-∧-inverse  ↦ ∧-inverse
+  not-∨-inverseˡ ↦ ∨-inverseˡ
+  not-∨-inverseʳ ↦ ∨-inverseʳ
+  not-∨-inverse  ↦ ∨-inverse
+
+  isCommutativeSemiring-∨-∧ ↦ ∨-∧-isCommutativeSemiring
+  commutativeSemiring-∨-∧   ↦ ∨-∧-commutativeSemiring
+  isCommutativeSemiring-∧-∨ ↦ ∧-∨-isCommutativeSemiring
+  commutativeSemiring-∧-∨   ↦ ∧-∨-commutativeSemiring
+  isBooleanAlgebra          ↦ ∨-∧-isBooleanAlgebra
+  booleanAlgebra            ↦ ∨-∧-booleanAlgebra
+  commutativeRing-xor-∧     ↦ xor-∧-commutativeRing
+
+  proof-irrelevance         ↦ T-irrelevance
+  ```
+
+* In `Data.Fin.Properties`:
+  ```agda
+  cmp              ↦ <-cmp
+  strictTotalOrder ↦ <-strictTotalOrder
+  ```
+
+* In `Data.Integer.Properties`:
+  ```agda
+  inverseˡ              ↦ +-inverseˡ
+  inverseʳ              ↦ +-inverseʳ
+  distribʳ              ↦ *-distribʳ-+
+  isCommutativeSemiring ↦ +-*-isCommutativeSemiring
+  commutativeRing       ↦ +-*-commutativeRing
+  *-+-right-mono        ↦ *-monoʳ-≤-pos
+  cancel-*-+-right-≤    ↦ *-cancelʳ-≤-pos
+  cancel-*-right        ↦ *-cancelʳ-≡
+  doubleNeg             ↦ neg-involutive
+  -‿involutive          ↦ neg-involutive
+  +-⊖-left-cancel       ↦ +-cancelˡ-⊖
+  ```
+
+* In `Data.List.Base`:
+  ```agda
+  gfilter ↦  mapMaybe
+  ```
+
+* In `Data.List.Properties`:
+  ```agda
+  right-identity-unique ↦ ++-identityʳ-unique
+  left-identity-unique  ↦ ++-identityˡ-unique
+  ```
+
+* In `Data.List.Relation.Pointwise`:
+  ```agda
+  Rel    ↦ Pointwise
+  Rel≡⇒≡ ↦ Pointwise-≡⇒≡
+  ≡⇒Rel≡ ↦ ≡⇒Pointwise-≡
+  Rel↔≡  ↦ Pointwise-≡↔≡
+  ```
+
+* In `Data.Nat.Properties`:
+  ```agda
+  ¬i+1+j≤i ↦ i+1+j≰i
+  ≤-steps  ↦ ≤-stepsˡ
+  ```
+
+* In all modules in the `Data.(Product/Sum).Relation` folders, all proofs with
+  names using infix notation have been deprecated in favour of identical
+  non-infix names, e.g.
+  ```
+  _×-isPreorder_ ↦ ×-isPreorder
+  ```
+
+* In `Data.Product.Relation.Lex.(Non)Strict`:
+  ```agda
+  ×-≈-respects₂ ↦ ×-respects₂
+  ```
+
+* In `Data.Product.Relation.Pointwise.Dependent`:
+  ```agda
+  Rel    ↦ Pointwise
+  Rel↔≡  ↦ Pointwise-≡↔≡
+  ```
+
+* In `Data.Product.Relation.Pointwise.NonDependent`:
+  ```agda
+  _×-Rel_         ↦ Pointwise
+  Rel↔≡           ↦ Pointwise-≡↔≡
+  _×-≈-respects₂_ ↦ ×-respects₂
+  ```
+
+* In `Data.Sign.Properties`:
+  ```agda
+  opposite-not-equal ↦ s≢opposite[s]
+  opposite-cong      ↦ opposite-injective
+  cancel-*-left      ↦ *-cancelˡ-≡
+  cancel-*-right     ↦ *-cancelʳ-≡
+  *-cancellative     ↦ *-cancel-≡
+  ```
+
+* In `Data.Vec.Properties`:
+  ```agda
+  proof-irrelevance-[]= ↦ []=-irrelevance
+  ```
+
+* In `Data.Vec.Relation.Pointwise.Inductive`:
+  ```agda
+  Pointwise-≡ ↦ Pointwise-≡↔≡
+  ```
+
+* In `Data.Vec.Relation.Pointwise.Extensional`:
+  ```agda
+  Pointwise-≡ ↦ Pointwise-≡↔≡
+  ```
+
+* In `Induction.Nat`:
+  ```agda
+  rec-builder      ↦ recBuilder
+  cRec-builder     ↦ cRecBuilder
+  <′-rec-builder   ↦ <′-recBuilder
+  <-rec-builder    ↦ <-recBuilder
+  ≺-rec-builder    ↦ ≺-recBuilder
+  <′-well-founded  ↦ <′-wellFounded
+  <′-well-founded′ ↦ <′-wellFounded′
+  <-well-founded   ↦ <-wellFounded
+  ≺-well-founded   ↦ ≺-wellFounded
+  ```
+
+* In `Induction.WellFounded`:
+  ```agda
+  Well-founded                       ↦ WellFounded
+  Some.wfRec-builder                 ↦ Some.wfRecBuilder
+  All.wfRec-builder                  ↦ All.wfRecBuilder
+  Subrelation.well-founded           ↦ Subrelation.wellFounded
+  InverseImage.well-founded          ↦ InverseImage.wellFounded
+  TransitiveClosure.downwards-closed ↦ TransitiveClosure.downwardsClosed
+  TransitiveClosure.well-founded     ↦ TransitiveClosure.wellFounded
+  Lexicographic.well-founded         ↦ Lexicographic.wellFounded
+  ```
+
+* In `Relation.Binary.PropositionalEquality`:
+  ```agda
+  proof-irrelevance     ↦ ≡-irrelevance
+  ```
+
+Removed features
+----------------
+
+#### Deprecated in version 0.10
+
+* Modules `Deprecated-inspect` and `Deprecated-inspect-on-steroids` in `Relation.Binary.PropositionalEquality`.
+
+* Module `Deprecated-inspect-on-steroids` in `Relation.Binary.HeterogeneousEquality`.
+
+Backwards compatible changes
+----------------------------
+
+* Added support for GHC 8.2.2.
+
+* New module `Data.Word` for new builtin type `Agda.Builtin.Word.Word64`.
+
+* New modules `Data.Table`, `Data.Table.Base`,
+  `Data.Table.Relation.Equality` and `Data.Table.Properties`. A `Table` is a
+  fixed-length collection of objects similar to a `Vec` from `Data.Vec`, but
+  implemented as a function `Fin n → A`. This prioritises ease of lookup as opposed
+  to `Vec` which prioritises the ease of adding and removing elements.
+
+* The contents of the following modules are now more polymorphic with respect to levels:
+  ```agda
+  Data.Covec
+  Data.List.Relation.Lex.Strict
+  Data.List.Relation.Lex.NonStrict
+  Data.Vec.Properties
+  Data.Vec.Relation.Pointwise.Inductive
+  Data.Vec.Relation.Pointwise.Extensional
+  ```
+
+* Added new proof to `asymmetric : Asymmetric _<_` to the `IsStrictPartialOrder` record.
+
+* Added new proofs to `Data.AVL`:
+  ```agda
+  leaf-injective     : leaf p ≡ leaf q → p ≡ q
+  node-injective-key : node k₁ lk₁ ku₁ bal₁ ≡ node k₂ lk₂ ku₂ bal₂ → k₁ ≡ k₂
+  node-injectiveˡ    : node k lk₁ ku₁ bal₁ ≡ node k lk₂ ku₂ bal₂ → lk₁ ≡ lk₂
+  node-injectiveʳ    : node k lk₁ ku₁ bal₁ ≡ node k lk₂ ku₂ bal₂ → ku₁ ≡ ku₂
+  node-injective-bal : node k lk₁ ku₁ bal₁ ≡ node k lk₂ ku₂ bal₂ → bal₁ ≡ bal₂
+  ```
+
+* Added new proofs to `Data.Bin`:
+  ```agda
+  less-injective : (b₁ < b₂ ∋ less lt₁) ≡ less lt₂ → lt₁ ≡ lt₂
+  ```
+
+* Added new proofs to `Data.Bool.Properties`:
+  ```agda
+  ∨-identityˡ           : LeftIdentity false _∨_
+  ∨-identityʳ           : RightIdentity false _∨_
+  ∨-identity            : Identity false _∨_
+  ∨-zeroˡ               : LeftZero true _∨_
+  ∨-zeroʳ               : RightZero true _∨_
+  ∨-zero                : Zero true _∨_
+  ∨-idem                : Idempotent _∨_
+  ∨-sel                 : Selective _∨_
+  ∨-isSemigroup         : IsSemigroup _≡_ _∨_
+  ∨-isCommutativeMonoid : IsCommutativeMonoid _≡_ _∨_ false
+
+  ∧-identityˡ           : LeftIdentity true _∧_
+  ∧-identityʳ           : RightIdentity true _∧_
+  ∧-identity            : Identity true _∧_
+  ∧-zeroˡ               : LeftZero false _∧_
+  ∧-zeroʳ               : RightZero false _∧_
+  ∧-zero                : Zero false _∧_
+  ∧-idem                : Idempotent _∧_
+  ∧-sel                 : Selective _∧_
+  ∧-isSemigroup         : IsSemigroup _≡_ _∧_
+  ∧-isCommutativeMonoid : IsCommutativeMonoid _≡_ _∧_ true
+
+  ∨-∧-isLattice             : IsLattice _≡_ _∨_ _∧_
+  ∨-∧-isDistributiveLattice : IsDistributiveLattice _≡_ _∨_ _∧_
+  ```
+
+* Added missing bindings to functions on `Data.Char.Base`:
+  ```agda
+  isLower    : Char → Bool
+  isDigit    : Char → Bool
+  isAlpha    : Char → Bool
+  isSpace    : Char → Bool
+  isAscii    : Char → Bool
+  isLatin1   : Char → Bool
+  isPrint    : Char → Bool
+  isHexDigit : Char → Bool
+  toNat      : Char → ℕ
+  fromNat    : ℕ → Char
+  ```
+
+* Added new proofs to `Data.Cofin`:
+  ```agda
+  suc-injective : (Cofin (suc m) ∋ suc p) ≡ suc q → p ≡ q
+  ```
+
+* Added new proofs to `Data.Colist`:
+  ```agda
+  ∷-injectiveˡ    : (Colist A ∋ x ∷ xs) ≡ y ∷ ys → x ≡ y
+  ∷-injectiveʳ    : (Colist A ∋ x ∷ xs) ≡ y ∷ ys → xs ≡ ys
+  here-injective  : (Any P (x ∷ xs) ∋ here p) ≡ here q → p ≡ q
+  there-injective : (Any P (x ∷ xs) ∋ there p) ≡ there q → p ≡ q
+  ∷-injectiveˡ    : (All P (x ∷ xs) ∋ px ∷ pxs) ≡ qx ∷ qxs → px ≡ qx
+  ∷-injectiveʳ    : (All P (x ∷ xs) ∋ px ∷ pxs) ≡ qx ∷ qxs → pxs ≡ qxs
+  ∷-injective     : (Finite (x ∷ xs) ∋ x ∷ p) ≡ x ∷ q → p ≡ q
+  ∷-injective     : (Infinite (x ∷ xs) ∋ x ∷ p) ≡ x ∷ q → p ≡ q
+  ```
+
+* Added new operations and proofs to `Data.Conat`:
+  ```agda
+  pred            : Coℕ → Coℕ
+
+  suc-injective   : (Coℕ ∋ suc m) ≡ suc n → m ≡ n
+  fromℕ-injective : fromℕ m ≡ fromℕ n → m ≡ n
+  suc-injective   : (suc m ≈ suc n ∋ suc p) ≡ suc q → p ≡ q
+  ```
+
+* Added new proofs to `Data.Covec`:
+  ```agda
+  ∷-injectiveˡ : (Covec A (suc n) ∋ a ∷ as) ≡ b ∷ bs → a ≡ b
+  ∷-injectiveʳ : (Covec A (suc n) ∋ a ∷ as) ≡ b ∷ bs → as ≡ bs
+  ```
+
+* Added new proofs to `Data.Fin.Properties`:
+  ```agda
+  ≤-isDecTotalOrder : ∀ {n} → IsDecTotalOrder _≡_ (_≤_ {n})
+  ≤-irrelevance     : ∀ {n} → IrrelevantRel (_≤_ {n})
+
+  <-asym            : ∀ {n} → Asymmetric (_<_ {n})
+  <-irrefl          : ∀ {n} → Irreflexive _≡_ (_<_ {n})
+  <-irrelevance     : ∀ {n} → IrrelevantRel (_<_ {n})
+  ```
+
+* Added new proofs to `Data.Integer.Properties`:
+  ```agda
+  +-cancelˡ-⊖       : (a + b) ⊖ (a + c) ≡ b ⊖ c
+  neg-minus-pos     : -[1+ m ] - (+ n) ≡ -[1+ (m + n) ]
+  [+m]-[+n]≡m⊖n     : (+ m) - (+ n) ≡ m ⊖ n
+  ∣m-n∣≡∣n-m∣       : ∣ m - n ∣ ≡ ∣ n - m ∣
+  +-minus-telescope : (m - n) + (n - o) ≡ m - o
+  pos-distrib-*     : ∀ x y → (+ x) * (+ y) ≡ + (x * y)
+
+  ≤-irrelevance     : IrrelevantRel _≤_
+  <-irrelevance     : IrrelevantRel _<_
+  ```
+
+* Added new combinators to `Data.List.Base`:
+  ```agda
+  lookup    : (xs : List A) → Fin (length xs) → A
+  unzipWith : (A → B × C) → List A → List B × List C
+  unzip     : List (A × B) → List A × List B
+  ```
+
+* Added new proofs to `Data.List.Properties`:
+  ```agda
+  ∷-injectiveˡ      : x ∷ xs ≡ y List.∷ ys → x ≡ y
+  ∷-injectiveʳ      : x ∷ xs ≡ y List.∷ ys → xs ≡ ys
+  ∷ʳ-injectiveˡ     : xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
+  ∷ʳ-injectiveʳ     : xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
+
+  ++-assoc          : Associative {A = List A} _≡_ _++_
+  ++-identityˡ      : LeftIdentity _≡_ [] _++_
+  ++-identityʳ      : RightIdentity _≡_ [] _++_
+  ++-identity       : Identity _≡_ [] _++_
+  ++-isSemigroup    : IsSemigroup {A = List A} _≡_ _++_
+  ++-isMonoid       : IsMonoid {A = List A} _≡_ _++_ []
+  ++-semigroup      : ∀ {a} (A : Set a) → Semigroup _ _
+  ++-monoid         : ∀ {a} (A : Set a) → Monoid _ _
+
+  filter-none       : All P xs     → dfilter P? xs ≡ xs
+  filter-some       : Any (∁ P) xs → length (filter P? xs) < length xs
+  filter-notAll     : Any P xs     → 0 < length (filter P? xs)
+  filter-all        : All (∁ P) xs → dfilter P? xs ≡ []
+  filter-complete   : length (filter P? xs) ≡ length xs → filter P? xs ≡ xs
+
+  tabulate-cong     : f ≗ g → tabulate f ≡ tabulate g
+  tabulate-lookup   : tabulate (lookup xs) ≡ xs
+
+  zipWith-identityˡ : ∀ xs → zipWith f [] xs ≡ []
+  zipWith-identityʳ : ∀ xs → zipWith f xs [] ≡ []
+  zipWith-comm      : (∀ x y → f x y ≡ f y x) → zipWith f xs ys ≡ zipWith f ys xs
+  zipWith-unzipWith : uncurry′ g ∘ f ≗ id → uncurry′ (zipWith g) ∘ (unzipWith f)  ≗ id
+  zipWith-map       : zipWith f (map g xs) (map h ys) ≡ zipWith (λ x y → f (g x) (h y)) xs ys
+  map-zipWith       : map g (zipWith f xs ys) ≡ zipWith (λ x y → g (f x y)) xs ys
+  length-zipWith    : length (zipWith f xs ys) ≡ length xs ⊓ length ys
+
+  length-unzipWith₁ : length (proj₁ (unzipWith f xys)) ≡ length xys
+  length-unzipWith₂ : length (proj₂ (unzipWith f xys)) ≡ length xys
+  ```
+
+* Added new proofs to `Data.List.All.Properties`:
+  ```agda
+  All-irrelevance : IrrelevantPred P → IrrelevantPred (All P)
+  filter⁺₁        : All P (filter P? xs)
+  filter⁺₂        : All Q xs → All Q (filter P? xs)
+  mapMaybe⁺       : All (Maybe.All P) (map f xs) → All P (mapMaybe f xs)
+  zipWith⁺        : Pointwise (λ x y → P (f x y)) xs ys → All P (zipWith f xs ys)
+  ```
+
+* Added new proofs to `Data.List.Any.Properties`:
+  ```agda
+  mapMaybe⁺ : Any (Maybe.Any P) (map f xs) → Any P (mapMaybe f xs)
+  ```
+
+* Added new proofs to `Data.List.Relation.Lex.NonStrict`:
+  ```agda
+  <-antisymmetric : Symmetric _≈_ → Antisymmetric _≈_ _≼_ → Antisymmetric _≋_ _<_
+  <-transitive    : IsPartialOrder _≈_ _≼_ → Transitive _<_
+  <-resp₂         : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ → _<_ Respects₂ _≋_
+
+  ≤-antisymmetric : Symmetric _≈_ → Antisymmetric _≈_ _≼_ → Antisymmetric _≋_ _≤_
+  ≤-transitive    : IsPartialOrder _≈_ _≼_ → Transitive _≤_
+  ≤-resp₂         : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ → _≤_ Respects₂ _≋_
+  ```
+
+* Added new proofs to `Data.List.Relation.Pointwise`:
+  ```agda
+  tabulate⁺ : (∀ i → f i ∼ g i) → Pointwise _∼_ (tabulate f) (tabulate g)
+  tabulate⁻ : Pointwise _∼_ (tabulate f) (tabulate g) → (∀ i → f i ∼ g i)
+  ++⁺       : Pointwise _∼_ ws xs → Pointwise _∼_ ys zs → Pointwise _∼_ (ws ++ ys) (xs ++ zs)
+  concat⁺   : Pointwise (Pointwise _∼_) xss yss → Pointwise _∼_ (concat xss) (concat yss)
+  ```
+
+* Added new proofs to `Data.List.Relation.Lex.Strict`:
+  ```agda
+  <-antisymmetric : Symmetric _≈_ → Irreflexive _≈_ _≺_ →  Asymmetric _≺_ → Antisymmetric _≋_ _<_
+  <-transitive    : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ → Transitive _≺_ → Transitive _<_
+  <-respects₂     : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ → _<_ Respects₂ _≋_
+
+  ≤-antisymmetric : Symmetric _≈_ → Irreflexive _≈_ _≺_ →  Asymmetric _≺_ → Antisymmetric _≋_ _≤_
+  ≤-transitive    : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ → Transitive _≺_ → Transitive _≤_
+  ≤-respects₂     : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ → _≤_ Respects₂ _≋_
+  ```
+
+* Added new proofs to `Data.Maybe.Base`:
+  ```agda
+  just-injective : (Maybe A ∋ just a) ≡ just b → a ≡ b
+  ```
+
+* Added new proofs to `Data.Nat.Divisibility`:
+  ```agda
+  m|m*n   : m ∣ m * n
+  ∣m⇒∣m*n : i ∣ m → i ∣ m * n
+  ∣n⇒∣m*n : i ∣ n → i ∣ m * n
+  ```
+
+* Added new proofs to `Data.Nat.Properties`:
+  ```agda
+  ≤⇒≯                   : _≤_ ⇒ _≯_
+  n≮n                   : ∀ n → n ≮ n
+  ≤-stepsʳ              : ∀ m ≤ n → m ≤ n + o
+  ≤-irrelevance         : IrrelevantRel _≤_
+  <-irrelevance         : IrrelevantRel _<_
+
+  +-monoˡ-≤             : ∀ n → (_+ n) Preserves _≤_ ⟶ _≤_
+  +-monoʳ-≤             : ∀ n → (n +_) Preserves _≤_ ⟶ _≤_
+  +-monoˡ-<             : ∀ n → (_+ n) Preserves _<_ ⟶ _<_
+  +-monoʳ-<             : ∀ n → (n +_) Preserves _<_ ⟶ _<_
+  +-semigroup           : Semigroup _ _
+  +-0-monoid            : Monoid _ _
+  +-0-commutativeMonoid : CommutativeMonoid _ _
+
+  *-monoˡ-≤             : ∀ n → (_* n) Preserves _≤_ ⟶ _≤_
+  *-monoʳ-≤             : ∀ n → (n *_) Preserves _≤_ ⟶ _≤_
+  *-semigroup           : Semigroup _ _
+  *-1-monoid            : Monoid _ _
+  *-1-commutativeMonoid : CommutativeMonoid _ _
+  *-+-semiring          : Semiring _ _
+
+  ^-identityʳ           : RightIdentity 1 _^_
+  ^-zeroˡ               : LeftZero 1 _^_
+  ^-semigroup-morphism  : (x ^_) Is +-semigroup -Semigroup⟶ *-semigroup
+  ^-monoid-morphism     : (x ^_) Is +-0-monoid -Monoid⟶ *-1-monoid
+
+  m≤n⇒m⊓n≡m             : m ≤ n → m ⊓ n ≡ m
+  m≤n⇒n⊓m≡m             : m ≤ n → n ⊓ m ≡ m
+  m≤n⇒n⊔m≡n             : m ≤ n → n ⊔ m ≡ n
+  m≤n⇒m⊔n≡n             : m ≤ n → m ⊔ n ≡ n
+  ⊔-monoˡ-≤             : ∀ n → (_⊔ n) Preserves _≤_ ⟶ _≤_
+  ⊔-monoʳ-≤             : ∀ n → (n ⊔_) Preserves _≤_ ⟶ _≤_
+  ⊓-monoˡ-≤             : ∀ n → (_⊓ n) Preserves _≤_ ⟶ _≤_
+  ⊓-monoʳ-≤             : ∀ n → (n ⊓_) Preserves _≤_ ⟶ _≤_
+  m∸n+n≡m               : n ≤ m → (m ∸ n) + n ≡ m
+  m∸[m∸n]≡n             : n ≤ m → m ∸ (m ∸ n) ≡ n
+
+  s≤s-injective         : s≤s p ≡ s≤s q → p ≡ q
+  ≤′-step-injective     : ≤′-step p ≡ ≤′-step q → p ≡ q
+  ```
+
+* Added new proofs to `Data.Plus`:
+  ```agda
+  []-injective    : (x [ _∼_ ]⁺ y ∋ [ p ]) ≡ [ q ] → p ≡ q
+  ∼⁺⟨⟩-injectiveˡ : (x [ _∼_ ]⁺ z ∋ x ∼⁺⟨ p ⟩ q) ≡ (x ∼⁺⟨ r ⟩ s) → p ≡ r
+  ∼⁺⟨⟩-injectiveʳ : (x [ _∼_ ]⁺ z ∋ x ∼⁺⟨ p ⟩ q) ≡ (x ∼⁺⟨ r ⟩ s) → q ≡ s
+  ```
+
+* Added new combinator to `Data.Product`:
+  ```agda
+  curry′ : (A × B → C) → (A → B → C)
+  ```
+
+* Added new proofs to `Data.Product.Properties`:
+  ```agda
+  ,-injectiveˡ : (a , b) ≡ (c , d) → a ≡ c
+  ,-injectiveʳ : (Σ A B ∋ (a , b)) ≡ (a , c) → b ≡ c
+  ```
+
+* Added new operator in `Data.Product.Relation.Pointwise.NonDependent`:
+  ```agda
+  _×ₛ_ : Setoid ℓ₁ ℓ₂ → Setoid ℓ₃ ℓ₄ → Setoid _ _
+  ```
+
+* Added new proofs to `Data.Rational.Properties`:
+  ```agda
+  ≤-irrelevance : IrrelevantRel _≤_
+  ```
+
+* Added new proofs to `Data.ReflexiveClosure`:
+  ```agda
+  []-injective : (Refl _∼_ x y ∋ [ p ]) ≡ [ q ] → p ≡ q
+  ```
+
+* Added new proofs to `Data.Sign`:
+  ```agda
+  *-isSemigroup : IsSemigroup _≡_ _*_
+  *-semigroup   : Semigroup _ _
+  *-isMonoid    : IsMonoid _≡_ _*_ +
+  *-monoid      : Monoid _ _
+  ```
+
+* Added new proofs to `Data.Star.Properties`:
+  ```agda
+  ◅-injectiveˡ : (Star T i k ∋ x ◅ xs) ≡ y ◅ ys → x ≡ y
+  ◅-injectiveʳ : (Star T i k ∋ x ◅ xs) ≡ y ◅ ys → xs ≡ ys
+  ```
+
+* Added new proofs to `Data.Sum.Properties`:
+  ```agda
+  inj₁-injective : (A ⊎ B ∋ inj₁ x) ≡ inj₁ y → x ≡ y
+  inj₂-injective : (A ⊎ B ∋ inj₂ x) ≡ inj₂ y → x ≡ y
+  ```
+
+* Added new operator in `Data.Sum.Relation.Pointwise`:
+  ```agda
+  _⊎ₛ_ : Setoid ℓ₁ ℓ₂ → Setoid ℓ₃ ℓ₄ → Setoid _ _
+  ```
+
+* Added new proofs to `Data.Vec.Properties`:
+  ```agda
+  ∷-injectiveˡ     : x ∷ xs ≡ y ∷ ys → x ≡ y
+  ∷-injectiveʳ     : x ∷ xs ≡ y ∷ ys → xs ≡ ys
+
+  []=⇒lookup       : xs [ i ]= x → lookup i xs ≡ x
+  lookup⇒[]=       : lookup i xs ≡ x → xs [ i ]= x
+  lookup-replicate : lookup i (replicate x) ≡ x
+  lookup-⊛         : lookup i (fs ⊛ xs) ≡ (lookup i fs $ lookup i xs)
+  tabulate-cong    : f ≗ g → tabulate f ≡ tabulate g
+  ```
+
+* Added new proofs to `Data.Vec.All.Properties`
+  ```agda
+  All-irrelevance : IrrelevantPred P → ∀ {n} → IrrelevantPred (All P {n})
+  ```
+
+* Added new proofs to `Data.Vec.Relation.Pointwise.Extensional`:
+  ```agda
+  isDecEquivalence      : IsDecEquivalence _~_ → IsDecEquivalence (Pointwise _~_)
+  extensional⇒inductive : Pointwise _~_ xs ys → IPointwise _~_ xs ys
+  inductive⇒extensional : IPointwise _~_ xs ys → Pointwise _~_ xs ys
+
+  ≡⇒Pointwise-≡         : Pointwise _≡_ xs ys → xs ≡ ys
+  Pointwise-≡⇒≡         : xs ≡ ys → Pointwise _≡_ xs ys
+  ```
+
+* Added new proofs to `Data.Vec.Relation.Pointwise.Inductive`:
+  ```agda
+  ++⁺              : Pointwise P xs → Pointwise P ys → Pointwise P (xs ++ ys)
+  ++⁻ˡ             : Pointwise P (xs ++ ys) → Pointwise P xs
+  ++⁻ʳ             : Pointwise P (xs ++ ys) → Pointwise P ys
+  ++⁻              : Pointwise P (xs ++ ys) → Pointwise P xs × Pointwise P ys
+
+  concat⁺          : Pointwise (Pointwise P) xss → Pointwise P (concat xss)
+  concat⁻          : Pointwise P (concat xss) → Pointwise (Pointwise P) xss
+
+  lookup           : Pointwise _~_ xs ys → ∀ i → lookup i xs ~ lookup i ys
+
+  isDecEquivalence : IsDecEquivalence _~_ → IsDecEquivalence (Pointwise _~_)
+
+  ≡⇒Pointwise-≡    : Pointwise _≡_ xs ys → xs ≡ ys
+  Pointwise-≡⇒≡    : xs ≡ ys → Pointwise _≡_ xs ys
+
+  Pointwiseˡ⇒All   : Pointwise (λ x y → P x) xs ys → All P xs
+  Pointwiseʳ⇒All   : Pointwise (λ x y → P y) xs ys → All P ys
+  All⇒Pointwiseˡ   : All P xs → Pointwise (λ x y → P x) xs ys
+  All⇒Pointwiseʳ   : All P ys → Pointwise (λ x y → P y) xs ys
+  ```
+
+* Added new functions and proofs to `Data.W`:
+  ```agda
+  map            : (f : A → C) → ∀[ D ∘ f ⇒ B ] → W A B → W C D
+  induction      : (∀ a {f} (hf : ∀ (b : B a) → P (f b)) → (w : W A B) → P w
+  foldr          : (∀ a → (B a → P) → P) → W A B → P
+
+  sup-injective₁ : sup x f ≡ sup y g → x ≡ y
+  sup-injective₂ : sup x f ≡ sup x g → f ≡ g
+  ```
+
+* Added new properties to `Relation.Binary.PropositionalEquality`
+  ```agda
+  isPropositional A = (a b : A) → a ≡ b
+  IrrelevantPred P  = ∀ {x} → isPropositional (P x)
+  IrrelevantRel _~_ = ∀ {x y} → isPropositional (x ~ y)
+  ```
+
+* Added new combinator to ` Relation.Binary.PropositionalEquality.TrustMe`:
+  ```agda
+  postulate[_↦_] : (t : A) → B t → (x : A) → B x
+  ```
+
+* Added new proofs to `Relation.Binary.StrictToNonStrict`:
+  ```agda
+  isPreorder₁     : IsPreorder _≈_ _<_ → IsPreorder _≈_ _≤_
+  isPreorder₂     : IsStrictPartialOrder _≈_ _<_ → IsPreorder _≈_ _≤_
+  isPartialOrder  : IsStrictPartialOrder _≈_ _<_ → IsPartialOrder _≈_ _≤_
+  isTotalOrder    : IsStrictTotalOrder _≈_ _<_ → IsTotalOrder _≈_ _≤_
+  isDecTotalOrder : IsStrictTotalOrder _≈_ _<_ → IsDecTotalOrder _≈_ _≤_
+  ```
+
+* Added new syntax, relations and proofs to `Relation.Unary`:
+  ```agda
+  syntax Universal P = ∀[ P ]
+
+  P ⊈  Q = ¬ (P ⊆ Q)
+  P ⊉  Q = ¬ (P ⊇ Q)
+  P ⊂  Q = P ⊆ Q × Q ⊈ P
+  P ⊃  Q = Q ⊂ P
+  P ⊄  Q = ¬ (P ⊂ Q)
+  P ⊅  Q = ¬ (P ⊃ Q)
+  P ⊈′ Q = ¬ (P ⊆′ Q)
+  P ⊉′ Q = ¬ (P ⊇′ Q)
+  P ⊂′ Q = P ⊆′ Q × Q ⊈′ P
+  P ⊃′ Q = Q ⊂′ P
+  P ⊄′ Q = ¬ (P ⊂′ Q)
+  P ⊅′ Q = ¬ (P ⊃′ Q)
+
+  f ⊢ P  = λ x → P (f x)
+
+  ∁? : Decidable P → Decidable (∁ P)
+  ```
+
+* Added `recompute` to `Relation.Nullary`:
+  ```agda
+  recompute : ∀ {a} {A : Set a} → Dec A → .A → A
+  ```
diff --git a/CHANGELOG/v0.16.md b/CHANGELOG/v0.16.md
new file mode 100644
index 0000000..13d6567
--- /dev/null
+++ b/CHANGELOG/v0.16.md
@@ -0,0 +1,651 @@
+Version 0.16
+============
+
+The library has been tested using Agda version 2.5.4.
+
+Important changes since 0.15:
+
+Non-backwards compatible changes
+--------------------------------
+
+#### Final overhaul of list membership
+
+* The aim of this final rearrangement of list membership is to create a better interface for
+  the different varieties of membership, and make it easier to predict where certain
+  proofs are found. Each of the new membership modules are parameterised by the relevant types
+  so as to allow easy access to the infix  `_∈_` and `_∈?_` operators. It also increases
+  the discoverability of the modules by new users of the library.
+
+* The following re-organisation of list membership modules has occurred:
+  ```agda
+  Data.List.Any.BagAndSetEquality        ↦ Data.List.Relation.BagAndSetEquality
+  Data.List.Any.Membership               ↦ Data.List.Membership.Setoid
+                                         ↘ Data.List.Membership.DecSetoid
+                                         ↘ Data.List.Relation.Sublist.Setoid
+  Data.List.Any.Membership.Propositional ↦ Data.List.Membership.Propositional
+                                         ↘ Data.List.Membership.DecPropositional
+                                         ↘ Data.List.Relation.Sublist.Propositional
+  ```
+
+* The `_⊆_` relation has been moved out of the `Membership` modules to new
+  modules `Data.List.Relation.Sublist.(Setoid/Propositional)`. Consequently the `mono`
+  proofs that were in `Data.List.Membership.Propositional.Properties` have been moved to
+  `Data.List.Relation.Sublist.Propositional.Properties`.
+
+* The following proofs have been moved from `Data.List.Any.Properties` to
+  `Data.List.Membership.Propositional.Properties.Core`:
+  ```agda
+  map∘find, find∘map, find-∈, lose∘find, find∘lose, ∃∈-Any, Any↔
+  ```
+
+* The following types and terms have been moved from `Data.List.Membership.Propositional` into
+  `Relation.BagAndSetEquality`:
+  ```agda
+  Kind, Symmetric-kind
+  set, subset, superset, bag, subbag, superbag
+  [_]-Order, [_]-Equality, _∼[_]_
+  ```
+
+* The type of the proof of `∈-resp-≈` in `Data.List.Membership.Setoid.Properties` has changed from
+  `∀ {x} → (x ≈_) Respects _≈_` to `∀ {xs} → (_∈ xs) Respects _≈_`.
+
+#### Upgrade of `Algebra.Operations`
+
+* Previously `Algebra.Operations` was parameterised by a semiring, however several of the
+  operators it defined depended only on the additive component. Therefore the modules have been
+  rearranged to allow more fine-grained use depending on the current position in the algebra
+  heirarchy. Currently there exist two modules:
+  ```
+  Algebra.Operations.CommutativeMonoid
+  Algebra.Operations.Semiring
+  ```
+  where `Algebra.Operations.Semiring` exports all the definitions previously exported
+  by `Algebra.Operations`. More modules may be added in future as required.
+
+  Also the fixity of `_×_`, `_×′_` and `_^_` have all been increased by 1.
+
+#### Upgrade of `takeWhile`, `dropWhile`, `span` and `break` in `Data.List`
+
+* These functions in `Data.List.Base` now use decidable
+  predicates instead of boolean-valued functions. The boolean versions discarded
+  type information, and hence were difficult to use and prove
+  properties about. The proofs have been updated and renamed accordingly.
+
+  The old boolean versions still exist as `boolTakeWhile`, `boolSpan` etc. for
+  backwards compatibility reasons, but are deprecated and may be removed in some
+  future release. The old versions can be implemented via the new versions
+  by passing the decidability proof `λ v → f v ≟ true` with `_≟_` from `Data.Bool`.
+
+#### Other
+
+* `Relation.Binary.Consequences` no longer exports `Total`. The standard way of accessing it
+  through `Relation.Binary` remains unchanged.
+
+* `_⇒_` in `Relation.Unary` is now right associative instead of left associative.
+
+* Added new module `Relation.Unary.Properties`. The following proofs have been moved
+  to the new module from `Relation.Unary`: `∅-Empty`, `∁∅-Universal`, `U-Universal`,
+  `∁U-Empty`, `∅-⊆`, `⊆-U` and `∁?`.
+
+* The set operations `_∩/∪_` in `Data.Fin.Subset` are now implemented more efficiently
+  using `zipWith _∧/∨_ p q` rather than `replicate _∧/∨_ ⊛ p ⊛ q`. The proof
+  `booleanAlgebra` has been moved to `∩-∪-booleanAlgebra` in `Data.Fin.Subset.Properties`.
+
+* The decidability proofs `_≟_` and `_<?_` are now exported by `Data.Fin` as well as
+  `Data.Fin.Properties` to improve consistency across the library. They may conflict with
+  `_≟_` and `_<?_` in `Data.Nat` or others. If so then it may be necessary to qualify imports
+  with either `using` or `hiding`.
+
+* Refactored and moved `↔Vec` from `Data.Product.N-ary` to `Data.Product.N-ary.Properties`.
+
+* Moved the function `reverse` and related proofs `reverse-prop`
+  `reverse-involutive` and `reverse-suc` from `Data.Fin.Properties` to the new
+  module `Data.Fin.Permutation.Components`.
+
+* Refactored `reverseView` in `Data.List.Reverse` to use a direct style instead
+  of the well-founded induction on the list's length that was used previously.
+
+* The function `filter` as implemented in `Data.List` has the semantics of _filter through_ rather
+  than _filter out_. The naming of proofs in `Data.List.Properties` used the latter rather than
+  the former and therefore the names of the proofs have been switched as follows:
+  ```agda
+  filter-none   ↦ filter-all
+  filter-some   ↦ filter-notAll
+  filter-notAll ↦ filter-some
+  filter-all    ↦ filter-none
+  ```
+
+Other major changes
+-------------------
+
+* The module `Algebra.Structures` can now be parameterised by equality in the same way
+  as `Algebra.FunctionProperties`. The structures within also now export a greater selection
+  of "left" and "right" properties. For example (where applicable):
+  ```agda
+  identityˡ : LeftIdentity ε _∙_
+  identityʳ : RightIdentity ε _∙_
+  inverseˡ  : LeftInverse ε _⁻¹ _∙_
+  inverseʳ  : RightInverse ε _⁻¹ _∙_
+  zeroˡ     : LeftZero 0# _*_
+  zeroʳ     : RightZero 0# _*_
+  distribˡ  : _*_ DistributesOverˡ _+_
+  distribʳ  : _*_ DistributesOverʳ _+_
+  ```
+
+* Added new modules `Data.Fin.Permutation` and `Data.Fin.Permutation.Components` for
+  reasoning about permutations. Permutations are implemented as bijections
+  `Fin m → Fin n`. `Permutation.Components` contains functions and proofs used to
+  implement these bijections.
+
+* Added new modules `Data.List.Zipper` and `Data.List.Zipper.Properties`.
+
+* Added a new module `Function.Reasoning` for creating multi-stage function pipelines.
+  See `README.Function.Reasoning` for examples.
+
+* Added new module `Relation.Binary.Indexed.Homogeneous`. This module defines
+  homogeneously-indexed binary relations, as opposed to the
+  heterogeneously-indexed binary relations found in `Relation.Binary.Indexed`.
+
+* Closures of binary relations have been centralised as follows:
+  ```agda
+  Data.ReflexiveClosure              ↦ Relation.Binary.Closure.Reflexive
+  Relation.Binary.SymmetricClosure   ↦ Relation.Binary.Closure.Symmetric
+  Data.Plus                          ↦ Relation.Binary.Closure.Transitive
+  Data.Star                          ↦ Relation.Binary.Closure.ReflexiveTransitive
+  Data.Star.Properties               ↦ Relation.Binary.Closure.ReflexiveTransitive.Properties
+  Relation.Binary.EquivalenceClosure ↦ Relation.Binary.Closure.Equivalence
+  ```
+  The old files still exist and re-export the contents of the new modules.
+
+
+Deprecated features
+-------------------
+
+The following renaming has occurred as part of a drive to improve consistency across
+the library. The old names still exist and therefore all existing code should still
+work, however they have been deprecated and use of the new names is encouraged. Although not
+anticipated any time soon, they may eventually be removed in some future release of the library.
+
+* In `Data.Fin.Properties`:
+  ```agda
+  to-from       ↦ toℕ-fromℕ
+  from-to       ↦ fromℕ-toℕ
+
+  bounded       ↦ toℕ<n
+  prop-toℕ-≤    ↦ toℕ≤pred[n]
+  prop-toℕ-≤′   ↦ toℕ≤pred[n]′
+
+  inject-lemma  ↦ toℕ-inject
+  inject+-lemma ↦ toℕ-inject+
+  inject₁-lemma ↦ toℕ-inject₁
+  inject≤-lemma ↦ toℕ-inject≤
+  ```
+
+* In `Data.List.All.Properties`:
+  ```agda
+  All-all ↦ all⁻
+  all-All ↦ all⁺
+  All-map ↦ map⁺
+  map-All ↦ map⁻
+  ```
+
+* In `Data.List.Membership.Propositional`:
+  ```agda
+  filter-∈ ↦ ∈-filter⁺
+  ```
+
+* In `Data.List.Membership.Setoid`:
+  ```agda
+  map-with-∈ ↦ mapWith∈
+  ```
+
+* In `Data.Vec.All.Properties`:
+  ```agda
+  All-map     ↦ map⁺
+  map-All     ↦ map⁻
+
+  All-++⁺     ↦ ++⁺
+  All-++ˡ⁻    ↦ ++ˡ⁻
+  All-++ʳ⁻    ↦ ++ʳ⁻
+  All-++⁻     ↦ ++⁻
+  All-++⁺∘++⁻ ↦ ++⁺∘++⁻
+  All-++⁻∘++⁺ ↦ ++⁻∘++⁺
+
+  All-concat⁺ ↦ concat⁺
+  All-concat⁻ ↦ concat⁻
+  ```
+
+* In `Relation.Binary.NonStrictToStrict`:
+  ```agda
+  irrefl         ↦ <-irrefl
+  trans          ↦ <-trans
+  antisym⟶asym   ↦ <-asym
+  decidable      ↦ <-decidable
+  trichotomous   ↦ <-trichotomous
+
+  isPartialOrder⟶isStrictPartialOrder ↦ <-isStrictPartialOrder
+  isTotalOrder⟶isStrictTotalOrder     ↦ <-isStrictTotalOrder₁
+  isDecTotalOrder⟶isStrictTotalOrder  ↦ <-isStrictTotalOrder₂
+  ```
+
+* In `IsStrictPartialOrder` record in `Relation.Binary`:
+  ```agda
+  asymmetric ↦ asym
+  ```
+
+Other minor additions
+---------------------
+
+* Added new records to `Algebra`:
+  ```agda
+  record Band c ℓ        : Set (suc (c ⊔ ℓ))
+  record Semilattice c ℓ : Set (suc (c ⊔ ℓ))
+  ```
+
+* Added new records to `Algebra.Structures`:
+  ```agda
+  record IsBand        (• : Op₂ A) : Set (a ⊔ ℓ)
+  record IsSemilattice (∧ : Op₂ A) : Set (a ⊔ ℓ)
+  ```
+
+* Added new functions to `Algebra.Operations.CommutativeMonoid`:
+  ```agda
+  sumₗ = List.foldr _+_ 0#
+  sumₜ = Table.foldr _+_ 0#
+  ```
+
+* Added new proofs to `Data.Bool.Properties`:
+  ```agda
+  ∧-semigroup                     : Semigroup _ _
+  ∧-commutativeMonoid             : CommutativeMonoid _
+  ∧-idempotentCommutativeMonoid   : IdempotentCommutativeMonoid _ _
+  ∧-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _∧_ true
+
+  ∨-semigroup                     : Semigroup _ _
+  ∨-commutativeMonoid             : CommutativeMonoid _ _
+  ∨-idempotentCommutativeMonoid   : IdempotentCommutativeMonoid _ _
+  ∨-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _∨_ false
+
+  ∨-∧-lattice                     : Lattice _ _
+  ∨-∧-distributiveLattice         : DistributiveLattice _ _
+  ```
+
+* Added new proofs to `Data.Fin.Properties`:
+  ```agda
+  ¬Fin0                  : ¬ Fin 0
+
+  ≤-preorder             : ℕ → Preorder _ _ _
+  ≤-poset                : ℕ → Poset _ _ _
+  ≤-totalOrder           : ℕ → TotalOrder _ _ _
+  ≤-decTotalOrder        : ℕ → DecTotalOrder _ _ _
+
+  <-respˡ-≡              : _<_ Respectsˡ _≡_
+  <-respʳ-≡              : _<_ Respectsʳ _≡_
+  <-resp₂-≡              : _<_ Respects₂ _≡_
+  <-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
+  <-strictPartialOrder   : ℕ → StrictPartialOrder _ _ _
+  <⇒≢                    : i < j → i ≢ j
+  ≤+≢⇒<                  : i ≤ j → i ≢ j → i < j
+  <⇒≤pred                : j < i → j ≤ pred i
+
+  toℕ‿ℕ-                 : toℕ (n ℕ- i) ≡ n ∸ toℕ i
+
+  inject₁-injective      : inject₁ i ≡ inject₁ j → i ≡ j
+
+  punchOut-cong          : j ≡ k → punchOut i≢j ≡ punchOut i≢k
+  punchOut-cong′         : punchOut i≢j ≡ punchOut (i≢j ∘ sym ∘ trans j≡k ∘ sym)
+  punchOut-punchIn       : punchOut (punchInᵢ≢i i j ∘ sym) ≡ j
+
+  ∀-cons                 : P zero → (∀ i → P (suc i)) → (∀ i → P i)
+  sequence⁻¹             : RawFunctor F → F (∀ i → P i) → (∀ i → F (P i))
+  ```
+
+* Added new functions to `Data.Fin.Subset`:
+  ```agda
+  ∣ p ∣ = count (_≟ inside) p
+  ```
+
+* Added new proofs to `Data.Fin.Subset.Properties`:
+  ```agda
+  ∣p∣≤n   : ∣ p ∣ ≤ n
+  ∣⊥∣≡0   : ∣ ⊥ ∣ ≡ 0
+  ∣⊤∣≡n   : ∣ ⊤ ∣ ≡ n
+  ∣⁅x⁆∣≡1 : ∣ ⁅ i ⁆ ∣ ≡ 1
+
+  ⊆-refl           : Reflexive _⊆_
+  ⊆-reflexive      : _≡_ ⇒ _⊆_
+  ⊆-trans          : Transitive _⊆_
+  ⊆-antisym        : Antisymmetric _≡_ _⊆_
+  ⊆-min            : Minimum _⊆_ ⊥
+  ⊆-max            : Maximum _⊆_ ⊤
+  ⊆-isPreorder     : IsPreorder _≡_ _⊆_
+  ⊆-preorder       : Preorder _ _ _
+  ⊆-isPartialOrder : IsPartialOrder _≡_ _⊆_
+  p⊆q⇒∣p∣<∣q∣      : ∀ {n} {p q : Subset n} → p ⊆ q → ∣ p ∣ ≤ ∣ q ∣
+
+  ∩-idem       : Idempotent _∩_
+  ∩-identityˡ  : LeftIdentity ⊤ _∩_
+  ∩-identityʳ  : RightIdentity ⊤ _∩_
+  ∩-identity   : Identity ⊤ _∩_
+  ∩-zeroˡ      : LeftZero ⊥ _∩_
+  ∩-zeroʳ      : RightZero ⊥ _∩_
+  ∩-zero       : Zero ⊥ _∩_
+  ∩-inverseˡ   : LeftInverse ⊥ ∁ _∩_
+  ∩-inverseʳ   : RightInverse ⊥ ∁ _∩_
+  ∩-inverse    : Inverse ⊥ ∁ _∩_
+  ∪-idem       : Idempotent _∪_
+  ∪-identityˡ  : LeftIdentity ⊥ _∪_
+  ∪-identityʳ  : RightIdentity ⊥ _∪_
+  ∪-identity   : Identity ⊥ _∪_
+  ∪-zeroˡ      : LeftZero ⊤ _∪_
+  ∪-zeroʳ      : RightZero ⊤ _∪_
+  ∪-zero       : Zero ⊤ _∪_
+  ∪-inverseˡ   : LeftInverse ⊤ ∁ _∪_
+  ∪-inverseʳ   : RightInverse ⊤ ∁ _∪_
+  ∪-inverse    : Inverse ⊤ ∁ _∪_
+  ∪-distribˡ-∩ : _∪_ DistributesOverˡ _∩_
+  ∪-distribʳ-∩ : _∪_ DistributesOverʳ _∩_
+  ∪-distrib-∩  : _∪_ DistributesOver _∩_
+  ∩-distribˡ-∪ : _∩_ DistributesOverˡ _∪_
+  ∩-distribʳ-∪ : _∩_ DistributesOverʳ _∪_
+  ∩-distrib-∪  : _∩_ DistributesOver _∪_
+  ∪-abs-∩      : _∪_ Absorbs _∩_
+  ∩-abs-∪      : _∩_ Absorbs _∪_
+
+  ∩-isSemigroup                   : IsSemigroup _∩_
+  ∩-semigroup                     : Semigroup _ _
+  ∩-isMonoid                      : IsMonoid _∩_ ⊤
+  ∩-monoid                        : Monoid _ _
+  ∩-isCommutativeMonoid           : IsCommutativeMonoid _∩_ ⊤
+  ∩-commutativeMonoid             : CommutativeMonoid _ _
+  ∩-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _∩_ ⊤
+  ∩-idempotentCommutativeMonoid   : IdempotentCommutativeMonoid _ _
+  ∪-isSemigroup                   : IsSemigroup _∪_
+  ∪-semigroup                     : Semigroup _ _
+  ∪-isMonoid                      : IsMonoid _∪_ ⊥
+  ∪-monoid                        : Monoid _ _
+  ∪-isCommutativeMonoid           : IsCommutativeMonoid _∪_ ⊥
+  ∪-commutativeMonoid             : CommutativeMonoid _ _
+  ∪-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _∪_ ⊥
+  ∪-idempotentCommutativeMonoid   : IdempotentCommutativeMonoid _ _
+  ∪-∩-isLattice                   : IsLattice _∪_ _∩_
+  ∪-∩-lattice                     : Lattice _ _
+  ∪-∩-isDistributiveLattice       : IsDistributiveLattice _∪_ _∩_
+  ∪-∩-distributiveLattice         : DistributiveLattice _ _
+  ∪-∩-isBooleanAlgebra            : IsBooleanAlgebra _∪_ _∩_ ∁ ⊤ ⊥
+  ∪-∩-booleanAlgebra              : BooleanAlgebra _ _
+  ∩-∪-isLattice                   : IsLattice _∩_ _∪_
+  ∩-∪-lattice                     : Lattice _ _
+  ∩-∪-isDistributiveLattice       : IsDistributiveLattice _∩_ _∪_
+  ∩-∪-distributiveLattice         : DistributiveLattice _ _
+  ∩-∪-isBooleanAlgebra            : IsBooleanAlgebra _∩_ _∪_ ∁ ⊥ ⊤
+  ∩-∪-booleanAlgebra              : BooleanAlgebra _ _
+  ```
+
+* Added new functions to `Data.List.All`:
+  ```agda
+  zip   : All P ∩ All Q ⊆ All (P ∩ Q)
+  unzip : All (P ∩ Q) ⊆ All P ∩ All Q
+  ```
+
+* Added new proofs to `Data.List.All.Properties`:
+  ```agda
+  singleton⁻ : All P [ x ] → P x
+  fromMaybe⁺ : Maybe.All P mx → All P (fromMaybe mx)
+  fromMaybe⁻ : All P (fromMaybe mx) → Maybe.All P mx
+  replicate⁺ : P x → All P (replicate n x)
+  replicate⁻ : All P (replicate (suc n) x) → P x
+  inits⁺     : All P xs → All (All P) (inits xs)
+  inits⁻     : All (All P) (inits xs) → All P xs
+  tails⁺     : All P xs → All (All P) (tails xs)
+  tails⁻     : All (All P) (tails xs) → All P xs
+  ```
+
+* Added new proofs to `Data.List.Membership.(Setoid/Propositional).Properties`:
+  ```agda
+  ∉-resp-≈      : ∀ {xs} → (_∉ xs) Respects _≈_
+  ∉-resp-≋      : ∀ {x}  → (x ∉_)  Respects _≋_
+
+  mapWith∈≗map  : mapWith∈ xs (λ {x} _ → f x) ≡ map f xs
+  mapWith∈-cong : (∀ x∈xs → f x∈xs ≡ g x∈xs) → mapWith∈ xs f ≡ map-with-∈ xs g
+
+  ∈-++⁺ˡ        : v ∈ xs → v ∈ xs ++ ys
+  ∈-++⁺ʳ        : v ∈ ys → v ∈ xs ++ ys
+  ∈-++⁻         : v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
+
+  ∈-concat⁺     : Any (v ∈_) xss → v ∈ concat xss
+  ∈-concat⁻     : v ∈ concat xss → Any (v ∈_) xss
+  ∈-concat⁺′    : v ∈ vs → vs ∈ xss → v ∈ concat xss
+  ∈-concat⁻′    : v ∈ concat xss → ∃ λ xs → v ∈ xs × xs ∈ xss
+
+  ∈-applyUpTo⁺  : i < n → f i ∈ applyUpTo f n
+  ∈-applyUpTo⁻  : v ∈ applyUpTo f n → ∃ λ i → i < n × v ≈ f i
+
+  ∈-tabulate⁺   : f i ∈ tabulate f
+  ∈-tabulate⁻   : v ∈ tabulate f → ∃ λ i → v ≈ f i
+
+  ∈-filter⁺     : P v → v ∈ xs → v ∈ filter P? xs
+  ∈-filter⁻     : v ∈ filter P? xs → v ∈ xs × P v
+
+  ∈-length      : x ∈ xs → 1 ≤ length xs
+  ∈-lookup      : lookup xs i ∈ xs
+
+  foldr-selective : Selective _≈_ _•_ → (foldr _•_ e xs ≈ e) ⊎ (foldr _•_ e xs ∈ xs)
+  ```
+
+* Added new function to `Data.List.NonEmpty`:
+  ```agda
+  fromList : List A → Maybe (List⁺ A)
+  ```
+
+* Added new proofs to `Data.List.Properties`:
+  ```agda
+  tabulate-cong   : f ≗ g → tabulate f ≡ tabulate g
+  tabulate-lookup : tabulate (lookup xs) ≡ xs
+
+  length-drop : length (drop n xs) ≡ length xs ∸ n
+  length-take : length (take n xs) ≡ n ⊓ (length xs)
+  ```
+
+* Added new proof to `Data.List.Relation.Pointwise`
+  ```agda
+  Pointwise-length : Pointwise _∼_ xs ys → length xs ≡ length ys
+  ```
+
+* Added new proofs to `Data.List.Relation.Sublist.(Setoid/Propositional).Properties`:
+  ```agda
+  ⊆-reflexive  : _≋_ ⇒ _⊆_
+  ⊆-refl       : Reflexive _⊆_
+  ⊆-trans      : Transitive _⊆_
+  ⊆-isPreorder : IsPreorder _≋_ _⊆_
+
+  filter⁺      : ∀ xs → filter P? xs ⊆ xs
+  ```
+
+* Added new proofs to `Data.Nat.Properties`:
+  ```agda
+  m+n≮m          : m + n ≮ m
+  m≮m∸n          : m ≮ m ∸ n
+
+  +-0-isMonoid   : IsMonoid _+_ 0
+  *-1-isMonoid   : IsMonoid _*_ 1
+
+  ⊓-triangulate  : x ⊓ y ⊓ z ≡ (x ⊓ y) ⊓ (y ⊓ z)
+  ⊔-triangulate  : x ⊔ y ⊔ z ≡ (x ⊔ y) ⊔ (y ⊔ z)
+
+  m∸n≡0⇒m≤n      : m ∸ n ≡ 0 → m ≤ n
+  m≤n⇒m∸n≡0      : m ≤ n → m ∸ n ≡ 0
+  ∸-monoˡ-≤      : m ≤ n → m ∸ o ≤ n ∸ o
+  ∸-monoʳ-≤      : m ≤ n → o ∸ m ≥ o ∸ n
+  ∸-distribˡ-⊓-⊔ : x ∸ (y ⊓ z) ≡ (x ∸ y) ⊔ (x ∸ z)
+  ∸-distribˡ-⊔-⊓ : x ∸ (y ⊔ z) ≡ (x ∸ y) ⊓ (x ∸ z)
+  ```
+
+* Added new functions to `Data.Product`:
+
+  ```agda
+  map₁ : (A → B) → A × C → B × C
+  map₂ : (∀ {x} → B x → C x) → Σ A B → Σ A C
+  ```
+
+* Added new functions to `Data.Product.N-ary`:
+  ```agda
+  _∈[_]_     : A → ∀ n → A ^ n → Set a
+  cons       : ∀ n → A → A ^ n → A ^ suc n
+  uncons     : ∀ n → A ^ suc n → A × A ^ n
+  head       : ∀ n → A ^ suc n → A
+  tail       : ∀ n → A ^ suc n → A ^ n
+  lookup     : ∀ (k : Fin n) → A ^ n → A
+  replicate  : ∀ n → A → A ^ n
+  tabulate   : ∀ n → (Fin n → A) → A ^ n
+  append     : ∀ m n → A ^ m → A ^ n → A ^ (m + n)
+  splitAt    : ∀ m n → A ^ (m + n) → A ^ m × A ^ n
+  map        : (A → B) → ∀ n → A ^ n → B ^ n
+  ap         : ∀ n → (A → B) ^ n → A ^ n → B ^ n
+  foldr      : P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (2+ n)) → ∀ n → A ^ n → P n
+  foldl      : P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (2+ n)) → ∀ n → A ^ n → P n
+  reverse    : ∀ n → A ^ n → A ^ n
+  zipWith    : (A → B → C) → ∀ n → A ^ n → B ^ n → C ^ n
+  unzipWith  : (A → B × C) → ∀ n → A ^ n → B ^ n × C ^ n
+  zip        : ∀ n → A ^ n → B ^ n → (A × B) ^ n
+  unzip      : ∀ n → (A × B) ^ n → A ^ n × B ^ n
+  ```
+
+* Added new proofs to `Data.Product.N-ary.Properties`:
+  ```agda
+  cons-head-tail-identity : cons n (head n as) (tail n as) ≡ as
+  head-cons-identity      : head n (cons n a as) ≡ a
+  tail-cons-identity      : tail n (cons n a as) ≡ as
+  append-cons-commute     : append (suc m) n (cons m a xs) ys ≡ cons (m + n) a (append m n xs ys)
+  append-splitAt-identity : uncurry (append m n) (splitAt m n as) ≡ as
+  ```
+
+* Added new functions to `Data.String.Base`:
+  ```agda
+  length    : String → ℕ
+  replicate : ℕ → Char → String
+  concat    : List String → String
+  ```
+
+* Added operator to `Data.Sum`:
+  ```agda
+  swap : A ⊎ B → B ⊎ A
+  ```
+  This may conflict with `swap` in `Data.Product`. If so then it may be necessary to
+  qualify imports with either `using` or `hiding`.
+
+* Added new proof to `Data.Sum.Properties`:
+  ```agda
+  swap-involutive : swap ∘ swap ≗ id
+  ```
+
+* Added new function to `Data.Vec`:
+  ```agda
+  count  : Decidable P → Vec A n → ℕ
+  insert : Fin (suc n) → A → Vec A n → Vec A (suc n)
+  remove : Fin (suc n) → Vec A (suc n) → Vec A n
+  ```
+
+* Added new proofs to `Data.Vec.Properties`:
+  ```agda
+  []=-injective     : xs [ i ]= x → xs [ i ]= y → x ≡ y
+  count≤n           : ∀ {n} (xs : Vec A n) → count P? xs ≤ n
+
+  ++-injectiveˡ     : (xs xs' : Vec A n) → xs ++ ys ≡ xs' ++ ys' → xs ≡ xs'
+  ++-injectiveʳ     : (xs xs' : Vec A n) → xs ++ ys ≡ xs' ++ ys' → ys ≡ ys'
+  ++-injective      : (xs xs' : Vec A n) → xs ++ ys ≡ xs' ++ ys' → xs ≡ xs' × ys ≡ ys'
+  ++-assoc          : (xs ++ ys) ++ zs ≅ xs ++ (ys ++ zs)
+
+  insert-lookup     : lookup i (insert i x xs) ≡ x
+  insert-punchIn    : lookup (punchIn i j) (insert i x xs) ≡ lookup j xs
+  remove-punchOut   : (i≢j : i ≢ j) → lookup (punchOut i≢j) (remove i xs) ≡ lookup j xs
+  remove-insert     : remove i (insert i x xs) ≡ xs
+  insert-remove     : insert i (lookup i xs) (remove i xs) ≡ xs
+
+  zipWith-assoc     : Associative _≡_ f → Associative _≡_ (zipWith f)
+  zipWith-comm      : (∀ x y → f x y ≡ f y x) → zipWith f xs ys ≡ zipWith f ys xs
+  zipWith-idem      : Idempotent _≡_ f → Idempotent _≡_ (zipWith f)
+  zipWith-identityˡ : LeftIdentity _≡_ 1# f → LeftIdentity _≡_ (replicate 1#) (zipWith f)
+  zipWith-identityʳ : RightIdentity _≡_ 1# f → RightIdentity _≡_ (replicate 1#) (zipWith f)
+  zipWith-zeroˡ     : LeftZero _≡_ 0# f → LeftZero _≡_ (replicate 0#) (zipWith f)
+  zipWith-zeroʳ     : RightZero _≡_ 0# f →  RightZero _≡_ (replicate 0#) (zipWith f)
+  zipWith-inverseˡ  : LeftInverse _≡_ 0# ⁻¹ f →  LeftInverse _≡_ (replicate 0#) (map ⁻¹) (zipWith f)
+  zipWith-inverseʳ  : RightInverse _≡_ 0# ⁻¹ f → RightInverse _≡_ (replicate 0#) (map ⁻¹) (zipWith f)
+  zipWith-distribˡ  : _DistributesOverˡ_ _≡_ f g → _DistributesOverˡ_ _≡_ (zipWith f) (zipWith g)
+  zipWith-distribʳ  : _DistributesOverʳ_ _≡_ f g → _DistributesOverʳ_ _≡_ (zipWith f) (zipWith g)
+  zipWith-absorbs   : _Absorbs_ _≡_ f g →  _Absorbs_ _≡_ (zipWith f) (zipWith g)
+
+  toList∘fromList   : toList (fromList xs) ≡ xs
+  ```
+
+* Added new types to `Relation.Binary.Core`:
+  ```agda
+  P Respectsʳ _∼_ = ∀ {x} → (P x)      Respects _∼_
+  P Respectsˡ _∼_ = ∀ {y} → (flip P y) Respects _∼_
+  ```
+  Records in `Relation.Binary` now export these in addition to the standard `Respects₂` proofs.
+  e.g. `IsStrictPartialOrder` exports:
+  ```agda
+  <-respˡ-≈ : _<_ Respectsˡ _≈_
+  <-respʳ-≈ : _<_ Respectsʳ _≈_
+  ```
+
+* Added new proof to `IsStrictTotalOrder` and `StrictTotalOrder` in `Relation.Binary`:
+  ```agda
+  asym : Asymmetric _<_
+  ```
+
+* Added `_≡⟨_⟩_` combinator  to `Relation.Binary.PreorderReasoning`.
+
+* Added new proofs to `Relation.Binary.NonStrictToStrict`:
+  ```agda
+  <-respˡ-≈ : _≤_ Respectsˡ _≈_ → _<_ Respectsˡ _≈_
+  <-respʳ-≈ : _≤_ Respectsʳ _≈_ → _<_ Respectsʳ _≈_
+
+  <-≤-trans : Transitive _≤_ → Antisymmetric _≈_ _≤_ → _≤_ Respectsʳ _≈_ → Trans _<_ _≤_ _<_
+  ≤-<-trans : Transitive _≤_ → Antisymmetric _≈_ _≤_ → _≤_ Respectsˡ _≈_ → Trans _≤_ _<_ _<_
+  ```
+
+* Added new proofs to `Relation.Binary.Consequences`:
+  ```agda
+  subst⟶respˡ : Substitutive _∼_ p → P Respectsˡ _∼_
+  subst⟶respʳ : Substitutive _∼_ p → P Respectsʳ _∼_
+
+  trans∧tri⟶respʳ≈ : Transitive _<_ → Trichotomous _≈_ _<_ → _<_ Respectsʳ _≈_
+  trans∧tri⟶respˡ≈ : Transitive _<_ → Trichotomous _≈_ _<_ → _<_ Respectsˡ _≈_
+  ```
+
+* Added new proof to `Relation.Binary.PropositionalEquality`:
+  ```agda
+  ≡-≟-identity : (eq : a ≡ b) → a ≟ b ≡ yes eq
+  ≢-≟-identity : a ≢ b → ∃ λ ¬eq → a ≟ b ≡ no ¬eq
+  ```
+
+* The types `Maximum` and `Minimum` are now exported by `Relation.Binary` as well
+  as `Relation.Binary.Lattice`.
+
+* Added new proofs to `Relation.Unary.Properties`:
+  ```agda
+  ⊆-refl  : Reflexive _⊆_
+  ⊆-trans : Transitive _⊆_
+  ⊂-asym  : Asymmetric _⊂_
+
+  _∪?_ : Decidable P → Decidable Q → Decidable (P ∪ Q)
+  _∩?_ : Decidable P → Decidable Q → Decidable (P ∩ Q)
+  _×?_ : Decidable P → Decidable Q → Decidable (P ⟨×⟩ Q)
+  _⊙?_ : Decidable P → Decidable Q → Decidable (P ⟨⊙⟩ Q)
+  _⊎?_ : Decidable P → Decidable Q → Decidable (P ⟨⊎⟩ Q)
+  _~?  : Decidable P → Decidable (P ~)
+  ```
+
+* Added indexed variants of functions to `Relation.Binary.HeterogeneousEquality`:
+  ```agda
+  icong                   : i ≡ j → (f : {k : I} → (z : A k) → B z) →
+                            x ≅ y → f x ≅ f y
+  icong₂                  : i ≡ j → (f : {k : I} → (z : A k) → (w : B z) → C z w) →
+                            x ≅ y → u ≅ v → f x u ≅ f y v
+  icong-subst-removable   : (eq : i ≅ j) (f : {k : I} → (z : A k) → B z) (x : A i) →
+                            f (subst A eq x) ≅ f x
+  icong-≡-subst-removable : (eq : i ≡ j) (f : {k : I} → (z : A k) → B z) (x : A i) →
+                            f (P.subst A eq x) ≅ f x
+  ```
author	Sean Whitton <spwhitton@spwhitton.name>	2018-11-23 17:29:46 -0700
committer	Sean Whitton <spwhitton@spwhitton.name>	2018-11-23 17:29:46 -0700
commit	5a91775bd7c909bbaf3b3c8ee964136961a5146d (patch)
tree	cea89f085c1382f1567ff71a30b6f953708dc6a9 /CHANGELOG
parent	5d2b156377dce5bdca65b14639306eaed3ac3a92 (diff)
parent	a19b25a865b2000bbd3acd909f5951a5407c1eec (diff)