Version 1.2
===========

The library has been tested using Agda version 2.6.0.1.

Highlights
----------

* New function hierarchy.

* New (homo/mono/iso)morphism infrastructure for algebraic and relational structures.

* Fresh lists.

* First proofs of algebraic properties for operations over ℚ.

* Improved reduction behaviour for all decidability proofs.

Bug-fixes
---------

* The record `RawRing` from `Algebra` now includes an equality relation to
  make it consistent with the othor `Raw` bundles.

* In `Relation.Binary`:
  - `IsStrictTotalOrder`      now exports `isDecStrictPartialOrder`
  - `IsDecStrictPartialOrder` now re-exports the contents of `IsStrictPartialOrder`.

* Due to bug #3879 in Agda, the pattern synonyms `0F`, `1F`, ... added to
  `Data.Fin.Base` in version 1.1 resulted in unavoidable and undesirable behaviour
  when case splitting on `ℕ` when `Data.Fin` has been imported. These pattern
  synonyms have therefore been moved to the new module `Data.Fin.Patterns`.

Non-backwards compatible changes
--------------------------------

### Standardisation of record hierarchies

* The modules containing the record hierarchies for algebra, binary relations,
  and functions are currently inconsistently structured. For example:
  - in the binary relation record hierarchy the module `Relation.Binary`
  exports all parts of the hierarchy, e.g. `Reflexive`, `IsPreorder` and
  `Preorder`.
  - in contrast the algebra record hierarchy `Associative` is exported
  from `Algebra.FunctionProperties`, `IsSemigroup` from `Algebra.Structures`
  and `Semigroup` from `Algebra`.
  - the function hiearchy doesn't have a notion of `Injective` and `IsInjective`
  at all, and `Injection` is exported from `Function.Injection`.

* Consequently all hierarchies have been re-organised to follow the
  same standard pattern:
  ```agda
  X.Core         -- Contains: Rel, Op₂, Fun etc.
  X.Definitions  -- Contains: Reflexive, Associative, Injective etc.
  X.Structures   -- Contains: IsEquivalence, IsSemigroup, IsInjection etc.
  X.Bundles      -- Contains: Setoid, Semigroup, Injection etc.
  X              -- Publicly re-exports all of the above
  ```

* In `Relation.Binary` this means:
  * New module `Relation.Binary.Bundles`
  * New module `Relation.Binary.Definitions`
  * Fully backwards compatible.

* In `Algebra` this means:
  * `Algebra.FunctionProperties.Core` has been deprecated in favour of `Algebra.Core`.
  * `Algebra.FunctionProperties` has been deprecated in favour of `Algebra.Definitions`.
  * The contents of `Algebra` has been moved to `Algebra.Bundles`.
  * `Algebra` now re-exports the contents of `Algebra.Definitions` and `Algebra.Structures`,
  not just that of `Algebra.Bundles`.
  * **Compatibility:** Modules which previously imported both `Algebra` and
  `Algebra.FunctionProperties` and/or `Algebra.Structures` will need small changes.
          - If either of `FunctionProperties` or `Structures` are explicitly parameterised by an
          equality relation then import `Algebra.Bundles` instead of `Algebra`.
          - Otherwise just remove the `FunctionProperties` and `Structures` imports entirely.

### New function hierarchy

* The problems with the current function hierarchy run deeper problems than the other two:
  1. The raw functions are wrapped in the equality-preserving
     type `_⟶_` from `Function.Equality`. As the rest of the library
     rarely uses such wrapped functions, it is very difficult
     to write code that interfaces neatly between the `Function` hierarchy
     and, for example, the `Algebra` hierarchy.
  2. The hierarchy doesn't follow the same pattern as the other record
     hierarchies in the standard library, e.g. `Injective`, `IsInjection`
     and `Injection`. Coupled with point 1., anecdotally this means that
     people find it difficult to understand and use.
  3. There is no way of specifying a function has a specific property
     (e.g. injectivity) without specifying all the properties required
     of the equality relation as well. This is in contrast to the
     `Relation.Binary` and `Algebra` hierarchies where it is perfectly
     possible to specify that for example an operation is commutative
     without providing all the proofs associated with the equality relation.
  4. In many fonts the symbol `_⟶_` used for equality preserving functions
     is almost indistinguishable from the symbol for ordinary functions `_→_`,
     leading to confusion when reading code.

* To address these problems a new standardised function hierarchy has been
  created that follows the same structure found in `Relation.Binary` and `Algebra`.
  In particular:
  - The `Fun1` and `Fun2` from `Function` have been moved to `Function.Core`.
  - The rest of the old contents of `Function` have been moved to `Function.Base`.
  - Added a new module `Function.Definitions` containing definitions like
        `Injective`, `Surjective` which are parameterised by the equality relations
    over the domain and codomain.
  - Added a new module `Function.Structures` containing definitions like
    `IsInjection`, `IsSurjection`, once again parameterised the equality relations.
  - New module `Function.Bundles` containing definitions like `Injection`, `Surjection`
    which provide essentially the same top-level interface as currently exists,
    i.e. parameterised by setoids but hiding the function.
  - The module `Function` now re-exports all of the above.

* For the moment the existing modules containing the old hierarchy still exist,
  as not all existing functionality has been reimplemented using the new hierarchy.
  However it is expected that they will be deprecated at some point in the future
  when contents this transfer is complete.
  ```agda
  Function.Equivalence
  Function.Equality
  Function.Bijection
  Function.Injection
  Function.Surjection
  Function.LeftInverse
  ```

* **Compatibility:** As most of changes involve adding new modules, the only problem
  that occurs is when importing both `Function` and e.g. `Function.Injection`. In this
  case the old and new definitions of `Injection` will clash. In the short term this
  can be fixed immediately by importing `Function.Base` instead of `Function`.
  However in the longer term it is encouraged to migrate away from `Function.Injection`
  and to use the new hierarchy instead.

* Finally the propositional bundle for left inverses in `Function.Bundles` has been
  renamed in the new hierarchy from `_↞_` to `_↩_`. This is in order to make room for
  the new bundle for right inverse `_↪_`.

#### Harmonizing `List.All` and `Vec` in their role as finite maps.

* The function `updateAt` in `Data.List.Relation.Unary.All` is analogous
  to `updateAt` in `Data.Vec.Base` and hence the API for the former has
  been refactored to match the latter.

* Added a new "points-to" relation `_[_]=_` in `Data.List.Relation.Unary.All`:
  ```agda
  _[_]=_ : All P xs → x ∈ xs → P x → Set _
  ```

* In `Data.List.Relation.Unary.All.Properties` the proofs `updateAt-cong`
  and `updateAt-updates` are now formulated in terms of the new `_[_]=_`
  relation rather than the function `lookup`. The old proofs are available with
  minor variations under the names `lookup∘updateAt` and `updateAt-cong-relative`.

#### Other

* Version 1.1 in the library added irrelevance to various places in the library.
  Unfortunately this exposed the library to several irrelevance-related bugs.
  The decision has therefore been taken to roll-back these additions until
  irrelevance is more stable. In particular it has been removed from
  `_%_`, `_/_`, `_div_`, `_mod_` in `Data.Nat.DivMod` and from `fromℕ≤`, `inject≤`
  in `Data.Fin.Base`.

* The proofs `isPreorder` and `preorder` have been moved from the `Setoid`
  record to the module `Relation.Binary.Properties.Setoid`.

* The function `normalize` in `Data.Rational.Base` has been reimplemented
  in terms of a direct division of the numerator and denominator by their
  GCD. Although less elegant than the previous implementation, it's
  reduction behaviour is much easier to reason about.

Re-implementations and deprecations
-------------------------------

### `Data.Bin` → `Data.Nat.Binary`

* The current implementation of binary naturals in Agda has proven hard to work with.
  Therefore a new, simpler implementation which avoids using `List` has been added
  as `Data.Nat.Binary`.
  ```agda
  Data.Nat.Binary
  Data.Nat.Binary.Base
  Data.Nat.Binary.Induction
  Data.Nat.Binary.Properties
  ```

* The old modules still exist but have been deprecated and may be removed in
  some future release of the library.
  ```agda
  Data.Bin
  Data.Bin.Properties
  ```

### `Data.Table` → `Data.Vec.Functional`

* As well as having a non-standard name, the definition of `Table` in `Data.Table`
  has proved very difficult to work with due to the wrapping of the type in a record.
  It has therefore been renamed and reimplemented without the record wrapper as the
  `Vector` type in the new module `Data.Vec.Functional`,
  ```agda
  Data.Vec.Functional
  Data.Vec.Functional.Relation.Binary.Pointwise
  Data.Vec.Functional.Relation.Unary.All
  Data.Vec.Functional.Relation.Unary.Any
  ```

* The old modules still exist but have been deprecated and may be removed in
  some future release of the library.
  ```agda
  Data.Table
  Data.Table.Base
  Data.Table.Properties
  Data.Table.Relation.Equality
  ```

### `Data.BoundedVec(.Inefficient)` → `Data.Vec.Bounded`

* `Data.BoundedVec` and `Data.BoundedVec.Inefficient` have been deprecated
  in favour of `Data.Vec.Bounded` introduced in version 1.1.
  ```agda
  Data.Vec.Bounded
  Data.Vec.Bounded.Base
  ```

* The old modules still exist but have been deprecated and may be removed in
  some future release of the library.
  ```agda
  Data.BoundedVec
  Data.BoundedVec.Inefficient
  ```

Other major additions
---------------------

### `Reflects` idiom for decidability proofs

* A version of the `Reflects` idiom, as seen in SSReflect, has been introduced
  in `Relation.Nullary`. Some properties of it have been added in the new module
  `Relation.Nullary.Reflects`. The definition is as follows
  ```agda
  data Reflects {p} (P : Set p) : Bool → Set p where
    ofʸ : ( p :   P) → Reflects P true
    ofⁿ : (¬p : ¬ P) → Reflects P false
  ```

* `Dec` has been redefined in terms of `Reflects`.
  ```agda
  record Dec {p} (P : Set p) : Set p where
    constructor _because_
    field
      does : Bool
      proof : Reflects P does

  open Dec public
  ```
  which is entirely backwards compatible thanks to the introduction of
  the pattern synonyms in `Relation.Nullary`:
  ```agda
  pattern yes p =  true because ofʸ  p
  pattern no ¬p = false because ofⁿ ¬p
  ```

* These changes mean that decision procedures can be defined so as to provide a
  boolean result that is independent of the proof that it is the correct decision.
  For example, a proof of decidability of `_≤_` on natural numbers:
    ```agda
  _≤?_ : (m n : ℕ) → Dec (m ≤ n)
  zero  ≤? n     = yes z≤n
  suc m ≤? zero  = no λ ()
  suc m ≤? suc n with m ≤? n
  ... | yes p = yes (s≤s p)
  ... | no ¬p = no  (¬p ∘ ≤-pred)
  ```
  can now be rewritten as:
  ```agda
  _≤?_ : (m n : ℕ) → Dec (m ≤ n)
  zero  ≤? n    = yes z≤n
  suc m ≤? zero = no λ ()
  does  (suc m ≤? suc n) = does (m ≤? n)
  proof (suc m ≤? suc n) with m ≤? n
  ... | yes p = ofʸ (s≤s p)
  ... | no ¬p = ofⁿ (¬p ∘ ≤-pred)
  ```
  Notice that projecting the `does` field, returns a function whose reduction
  behaviour is identically to what we would expect of a boolean test. This has
  significant advantages for both performance and reasoning in situations where
  only a decision is required and the proof itself is not needed.

* Functions and lemmas about `Dec` have been rewritten to reflect these changes.
  - The lemmas `map′` and `map` in `Relation.Nullary.Decidable` produce their
  `does` result without any pattern matching, and `isYes` matches only on the
  `does` field, and not the `proof` field. For example this means that
  `does (map f X?)` is definitionally equal to `does X?`.
  - All of the connective lemmas like `_×-dec_` have a `does`
  field written in terms of boolean functions like `_∧_`. As well as being
  less strict than the previous definitions, this should improve readability
  when only the `does` field is involved.

* The function `⌊_⌋` still exists to be used in conjunction with `toWitness`
  and similar (e.g. in proof automation), but doesn't require the immediate
  evaluation of the `proof` part.

* The rest of the `Relation.Nullary` subtree has been updated to reflect the
  changes to `Dec`.

### Other new modules

* Properties for `Semigroup` and `CommutativeSemigroup`. Contains all the
  non-trivial 3 element permutations. Useful for equational reasoning.
  ```agda
  Algebra.Properties.Semigroup
  Algebra.Properties.CommutativeSemigroup
  ```


* A map interface for AVL trees.
  ```agda
  Data.AVL.Map
  ```

* Level polymorphic versions for the bottom and top types. Useful in
  getting rid of the need to use `Lift`.
  ```agda
  Data.Unit.Polymorphic
  Data.Unit.Polymorphic.Properties
  Data.Empty.Polymorphic
  ```


* Greatest common divisor and least common multiples for integers:
  ```agda
  Data.Integer.GCD
  Data.Integer.LCM
  ```

* Fresh lists.
  ```agda
  Data.List.Fresh
  Data.List.Fresh.Properties
  Data.List.Fresh.Relation.Unary.All
  Data.List.Fresh.Relation.Unary.All.Properties
  Data.List.Fresh.Relation.Unary.Any
  Data.List.Fresh.Relation.Unary.Any.Properties
  Data.List.Fresh.Membership
  Data.List.Fresh.Membership.Properties
  ```

* Kleene lists. Useful when needing to distinguish between empty and non-empty lists.
  ```agda
  Data.List.Kleene
  Data.List.Kleene.AsList
  Data.List.Kleene.Base
  ```


* Predicate over lists in which every neighbouring pair of elements is related.
  Useful for implementing paths in graphs.
  ```agda
  Data.List.Relation.Unary.Linked
  Data.List.Relation.Unary.Linked.Properties
  ```

* Disjoint sublists.
  ```agda
  Data.List.Relation.Binary.Sublist.Propositional.Disjoint
  ```

* Rationals whose numerator and denominator are not necessarily normalised (i.e. coprime).
  ```
  Data.Rational.Unnormalised
  Data.Rational.Unnormalised.Properties
  ```
  In this formalisation every number has an infinite number of multiple representations
  and that evaluation is inefficient as the top and the bottom will inevitably
  blow up. However they are significantly easier to reason about then the existing
  normalised implementation in `Data.Rational`. The new monomorphism infrastructure
  (see below) is used to transfer proofs from these new unnormalised rationals
  to the existing normalised implementation.

* Basic constructions for the new funciton hierarchy.
  ```agda
  Function.Construct.Identity
  Function.Construct.Composition
  ```

* New interfaces for using Haskell datatypes:
  ```
  Foreign.Haskell.Coerce
  Foreign.Haskell.Either
  ```

* Properties of setoids.
  ```agda
  Relation.Binary.Properties.Setoid
  ```

* Reasoning over partial setoids.
  ```
  Relation.Binary.Reasoning.Base.Partial
  Relation.Binary.Reasoning.PartialSetoid
  ```

* Morphisms between algebraic and relational structures. See
  `Data.Rational.Properties` for how these can be used to easily transfer
  algebraic properties from unnormalised to normalised rationals.
  ```agda
  Algebra.Morphism.Definitions
  Algebra.Morphism.Structures
  Algebra.Morphism.MagmaMonomorphism
  Algebra.Morphism.MonoidMonomorphism

  Relation.Binary.Morphism
  Relation.Binary.Morphism.Definitions
  Relation.Binary.Morphism.Structures
  Relation.Binary.Morphism.RelMonomorphism
  Relation.Binary.Morphism.OrderMonomorphism
  ```

Deprecated names
----------------

The following deprecations have occurred as part of a drive to improve
consistency across the library. The deprecated names still exist and
therefore all existing code should still work, however 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. Automated warnings are
attached to all deprecated names to discourage their use.

* In `Data.Fin`:
  ```agda
  fromℕ≤  ↦ fromℕ<
  fromℕ≤″ ↦ fromℕ<″
  ```

* In `Data.Fin.Properties`
  ```agda
  fromℕ≤-toℕ       ↦ fromℕ<-toℕ
  toℕ-fromℕ≤       ↦ toℕ-fromℕ<
  fromℕ≤≡fromℕ≤″   ↦ fromℕ<≡fromℕ<″
  toℕ-fromℕ≤″      ↦ toℕ-fromℕ<″
  isDecEquivalence ↦ ≡-isDecEquivalence
  preorder         ↦ ≡-preorder
  setoid           ↦ ≡-setoid
  decSetoid        ↦ ≡-decSetoid
  ```

* In `Data.Integer.Properties`:
  ```agda
  [1+m]*n≡n+m*n ↦ suc-*
  ```

* In `Data.Nat.Coprimality`:
  ```agda
  coprime-gcd ↦ coprime⇒GCD≡1
  gcd-coprime ↦ GCD≡1⇒coprime
  ```

* In `Data.Nat.Properties`:
  ```agda
  +-*-suc ↦ *-suc
  n∸m≤n   ↦ m∸n≤m
  ```
  (Note that the latter will require the arguments to be reversed)

* In `Data.Unit` the definition `_≤_` is unnecessary as it is isomorphic to `_≡_`
  and has therefore been deprecated.

* In `Data.Unit.Properties` the associated proofs have therefore been renamed as follows:
  ```agda
  ≤-total           ↦ ≡-total
  _≤?_              ↦ _≟_
  ≤-isPreorder      ↦ ≡-isPreorder
  ≤-isPartialOrder  ↦ ≡-isPartialOrder
  ≤-isTotalOrder    ↦ ≡-isTotalOrder
  ≤-isDecTotalOrder ↦ ≡-isDecTotalOrder
  ≤-poset           ↦ ≡-poset
  ≤-decTotalOrder   ↦ ≡-decTotalOrder
  ```

* In `Relation.Binary.Properties.Poset`:
  ```agda
  invIsPartialOrder  ↦ ≥-isPartialOrder
  invPoset           ↦ ≥-poset
  strictPartialOrder ↦ <-strictPartialOrder
  ```

* In `Relation.Binary.Properties.DecTotalOrder`:
  ```agda
  strictTotalOrder ↦ <-strictTotalOrder
  ```

Other minor additions
---------------------

* Added new definition to `Algebra.Bundles`:
  ```agda
  record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ))
  ```

* Added new definition to `Algebra.Structures`:
  ```agda
  record IsCommutativeSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ)
  ```

* The function `tail` in `Codata.Stream` has a new, more general type:
  ```agda
  tail : ∀ {i} {j : Size< i} → Stream A i → Stream A j
  ```

* Added new proofs to `Data.Char.Properties`:
  ```agda
  <-isStrictPartialOrder-≈ : IsStrictPartialOrder _≈_ _<_
  <-isStrictTotalOrder-≈   : IsStrictTotalOrder _≈_ _<_
  <-strictPartialOrder-≈   : StrictPartialOrder 0ℓ 0ℓ 0ℓ
  ```

* Added new proofs to `Data.Fin.Properties`:
  ```agda
  ∀-cons-⇔ : (P zero × Π[ P ∘ suc ]) ⇔ Π[ P ]
  ∃-here   : P zero → ∃⟨ P ⟩
  ∃-there  : ∃⟨ P ∘ suc ⟩ → ∃⟨ P ⟩
  ∃-toSum  : ∃⟨ P ⟩ → P zero ⊎ ∃⟨ P ∘ suc ⟩
  ⊎⇔∃      : (P zero ⊎ ∃⟨ P ∘ suc ⟩) ⇔ ∃⟨ P ⟩
  ```

* Added new proofs to `Data.Fin.Subset.Properties`:
  ```agda
  out⊆          : p ⊆ q → outside ∷ p ⊆      y ∷ q
  out⊆-⇔        : p ⊆ q ⇔ outside ∷ p ⊆      y ∷ q
  in⊆in         : p ⊆ q →  inside ∷ p ⊆ inside ∷ q
  in⊆in-⇔       : p ⊆ q ⇔  inside ∷ p ⊆ inside ∷ q

  ∃-Subset-zero : ∃⟨ P ⟩ → P []
  ∃-Subset-[]-⇔ : P [] ⇔ ∃⟨ P ⟩
  ∃-Subset-suc  : ∃⟨ P ⟩ → ∃⟨ P ∘ (inside ∷_) ⟩ ⊎ ∃⟨ P ∘ (outside ∷_) ⟩
  ∃-Subset-∷-⇔  : (∃⟨ P ∘ (inside ∷_) ⟩ ⊎ ∃⟨ P ∘ (outside ∷_) ⟩) ⇔ ∃⟨ P ⟩
  ```

* Added new constants to `Data.Integer.Base`:
  ```agda
  -1ℤ = -[1+ 0 ]
   0ℤ = +0
   1ℤ = +[1+ 0 ]
  ```

* Added new proofs to `Data.Integer.Properties`:
  ```agda
  *-suc : m * sucℤ n ≡ m + m * n

  +-isCommutativeSemigroup : IsCommutativeSemigroup _+_
  *-isCommutativeSemigroup : IsCommutativeSemigroup _*_
  +-commutativeSemigroup   : CommutativeSemigroup 0ℓ 0ℓ
  *-commutativeSemigroup   : CommutativeSemigroup 0ℓ 0ℓ
  ```

* Added new function to `Data.List.Base`:
  ```agda
  _ʳ++_ = flip reverseAcc
  ```

* Added new proofs to `Data.List.Properties`:
  ```agda
  filter-accept : P x → filter P? (x ∷ xs) ≡ x ∷ (filter P? xs)
  filter-reject : ¬ P x → filter P? (x ∷ xs) ≡ filter P? xs
  filter-idem   : filter P? ∘ filter P? ≗ filter P?
  filter-++     : filter P? (xs ++ ys) ≡ filter P? xs ++ filter P? ys

  ʳ++-defn   : xs ʳ++ ys ≡ reverse xs ++ ys
  ʳ++-++     : (xs ++ ys) ʳ++ zs ≡ ys ʳ++ xs ʳ++ zs
  ʳ++-ʳ++    : (xs ʳ++ ys) ʳ++ zs ≡ ys ʳ++ xs ++ zs
  length-ʳ++ : length (xs ʳ++ ys) ≡ length xs + length ys
  map-ʳ++    : map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys
  foldr-ʳ++  : foldr f b (xs ʳ++ ys) ≡ foldl (flip f) (foldr f b ys) xs
  foldl-ʳ++  : foldl f b (xs ʳ++ ys) ≡ foldl f (foldr (flip f) b xs) ys
  ```

* Added new definitions to `Data.List.Relation.Binary.Lex.Core`:
  ```agda
  []<[]-⇔ : P ⇔ [] < []
  toSum   : (x ∷ xs) < (y ∷ ys) → (x ≺ y ⊎ (x ≈ y × xs < ys))
  ∷<∷-⇔   : (x ≺ y ⊎ (x ≈ y × xs < ys)) ⇔ (x ∷ xs) < (y ∷ ys)
  ```

* The proof `toAny` in `Data.List.Relation.Binary.Sublist.Heterogeneous` has a new more general type:
  ```agda
  toAny : Sublist R (a ∷ as) bs → Any (R a) bs
  ```

* Added new relations to `Data.List.Relation.Binary.Sublist.Heterogeneous`:
  ```agda
  Disjoint (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs)
  DisjointUnion (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) (τ : xys ⊆ zs)
  ```

* Added new relations and definitions to `Data.List.Relation.Binary.Sublist.Setoid`:
  ```agda
  xs ⊇ ys = ys ⊆ xs
  xs ⊈ ys = ¬ (xs ⊆ ys)
  xs ⊉ ys = ¬ (xs ⊇ ys)

  UpperBound (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs)
  ⊆-disjoint-union : Disjoint τ σ → UpperBound τ σ
  ```

* Added new proofs to `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
  ```agda
  shrinkDisjointˡ : Disjoint τ₁ τ₂ → Disjoint (⊆-trans σ τ₁) τ₂
  shrinkDisjointʳ : Disjoint τ₁ τ₂ → Disjoint τ₁ (⊆-trans σ τ₂)
  ```

* Added new definitions to `Data.List.Relation.Binary.Sublist.Propositional`:
  ```agda
  separateˡ : (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → Separation τ₁ τ₂
  ```

* Added new proofs to `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
  ```agda
  ⊆-trans-idˡ      : ⊆-trans ⊆-refl τ ≡ τ
  ⊆-trans-idʳ      : ⊆-trans τ ⊆-refl ≡ τ
  ⊆-trans-assoc    : ⊆-trans τ₁ (⊆-trans τ₂ τ₃) ≡ ⊆-trans (⊆-trans τ₁ τ₂) τ₃
  All-resp-⊆       : (All P) Respects _⊇_
  Any-resp-⊆       : (Any P) Respects _⊆_
  All-resp-⊆-refl  : All-resp-⊆ ⊆-refl ≗ id
  All-resp-⊆-trans : All-resp-⊆ (⊆-trans τ τ′) ≗ All-resp-⊆ τ ∘ All-resp-⊆ τ′
  Any-resp-⊆-refl  : Any-resp-⊆ ⊆-refl ≗ id
  Any-resp-⊆-trans : Any-resp-⊆ (⊆-trans τ τ′) ≗ Any-resp-⊆ τ′ ∘ Any-resp-⊆ τ
  lookup-injective : lookup τ i ≡ lookup τ j → i ≡ j
  ```

* Added new definition to `Data.List.Relation.Binary.Pointwise`:
  ```agda
  uncons : Pointwise _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y × Pointwise _∼_ xs ys
  ```

* Added new definitions to `Data.List.Relation.Unary.All`:
  ```agda
  Null = All (λ _ → ⊥)
  ```

* Added new proofs to `Data.List.Relation.Unary.All.Properties`:
  ```agda
  Null⇒null     : Null xs → T (null xs)
  null⇒Null     : T (null xs) → Null xs

  []=-injective : pxs [ i ]= px → pxs [ i ]= qx → px ≡ qx
  []=lookup     : (i : x ∈ xs) → pxs [ i ]= lookup pxs i
  []=⇒lookup    : pxs [ i ]= px → lookup pxs i ≡ px
  lookup⇒[]=    : lookup pxs i ≡ px → pxs [ i ]= px

  updateAt-minimal          : i ≢∈ j → pxs [ i ]= px → updateAt j f pxs [ i ]= px
  updateAt-id-relative      : f (lookup pxs i) ≡ lookup pxs i → updateAt i f pxs ≡ pxs
  updateAt-compose-relative : f (g (lookup pxs i)) ≡ h (lookup pxs i) → updateAt i f (updateAt i g pxs) ≡ updateAt i h pxs
  updateAt-commutes         : i ≢∈ j → updateAt i f ∘ updateAt j g ≗ updateAt j g ∘ updateAt i f
  ```

* The proof `All-swap` in `Data.List.Relation.Unary.All.Properties` has been generalised to work over `_~_ : REL A B ℓ` instead of just `_~_ : REL (List A) B ℓ`.

* Added new definition to `Data.List.Relation.Unary.AllPairs`:
  ```agda
  uncons : AllPairs R (x ∷ xs) → All (R x) xs × AllPairs R xs
  ```

* Added new proofs to `Data.Nat.Coprimality`:
  ```agda
  coprime⇒gcd≡1 : Coprime m n → gcd m n ≡ 1
  gcd≡1⇒coprime : gcd m n ≡ 1 → Coprime m n
  coprime-/gcd  : Coprime (m / gcd m n) (n / gcd m n)
  ```

* Added new proof to `Data.Nat.Divisibility`:
  ```agda
  >⇒∤ : m > suc n → m ∤ suc n
  ```

* Added new proofs to `Data.Nat.DivMod`:
  ```agda
  /-congˡ   : m ≡ n → m / o ≡ n / o
  /-congʳ   : n ≡ o → m / n ≡ m / o
  /-mono-≤  : m ≤ n → o ≥ p → m / o ≤ n / p
  /-monoˡ-≤ : m ≤ n → m / o ≤ n / o
  /-monoʳ-≤ : n ≥ o → m / n ≤ m / o
  m≥n⇒m/n>0 : m ≥ n → m / n > 0
  ```

* Added new proofs to `Data.Nat.GCD`:
  ```agda
  gcd[m,n]≡0⇒m≡0 : gcd m n ≡ 0 → m ≡ 0
  gcd[m,n]≡0⇒n≡0 : gcd m n ≡ 0 → n ≡ 0
  gcd[m,n]≤n     : gcd m (suc n) ≤ suc n
  n/gcd[m,n]≢0   : {n≢0 gcd≢0} → n / gcd m n ≢ 0
  GCD-*          : GCD (m * suc c) (n * suc c) (d * suc c) → GCD m n d
  GCD-/          : c ∣ m → c ∣ n → c ∣ d → GCD m n d → GCD (m / c) (n / c) (d / c)
  GCD-/gcd       : GCD (m / gcd m n) (n / gcd m n) 1
  ```

* Added new proofs to `Data.Nat.Properties`:
  ```agda
  0≢1+n          : 0 ≢ suc n
  1+n≢n          : suc n ≢ n
  even≢odd       : 2 * m ≢ suc (2 * n)

  0<1+n          : 0 < suc n
  n<1+n          : n < suc n
  m<m+n          : n > 0 → m < m + n
  m<n⇒n≢0        : m < n → n ≢ 0
  m<n⇒m≤1+n      : m < n → m ≤ suc n
  m≤n⇒m<n∨m≡n    : m ≤ n → m < n ⊎ m ≡ n
  ∀[m≤n⇒m≢o]⇒o<n : (∀ {m} → m ≤ n → m ≢ o) → n < o
  ∀[m<n⇒m≢o]⇒o≤n : (∀ {m} → m < n → m ≢ o) → n ≤ o

  +-rawMagma     : RawMagma 0ℓ 0ℓ
  *-rawMagma     : RawMagma 0ℓ 0ℓ
  +-0-rawMonoid  : RawMonoid 0ℓ 0ℓ
  *-1-rawMonoid  : RawMonoid 0ℓ 0ℓ

  *-cancelˡ-≤    : suc o * m ≤ suc o * n → m ≤ n

  1+m≢m∸n        : suc m ≢ m ∸ n
  ∸-monoʳ-<      : o < n → n ≤ m → m ∸ n < m ∸ o
  ∸-cancelʳ-≤    : m ≤ o → o ∸ n ≤ o ∸ m → m ≤ n
  ∸-cancelʳ-<    : o ∸ m < o ∸ n → n < m
  ∸-cancelˡ-≡    : n ≤ m → o ≤ m → m ∸ n ≡ m ∸ o → n ≡ o
  m<n⇒0<n∸m      : m < n → 0 < n ∸ m
  m>n⇒m∸n≢0      : m > n → m ∸ n ≢ 0

  ∣-∣-identityˡ  : LeftIdentity 0 ∣_-_∣
  ∣-∣-identityʳ  : RightIdentity 0 ∣_-_∣
  ∣-∣-identity   : Identity 0 ∣_-_∣
  m≤n+∣n-m∣      : m ≤ n + ∣ n - m ∣
  m≤n+∣m-n∣      : m ≤ n + ∣ m - n ∣
  m≤∣m-n∣+n      : m ≤ ∣ m - n ∣ + n

  +-isCommutativeSemigroup : IsCommutativeSemigroup _+_
  +-commutativeSemigroup   : CommutativeSemigroup 0ℓ 0ℓ
  ```

* Added new bundles to `Data.String.Properties`:
  ```agda
  <-isStrictPartialOrder-≈ : IsStrictPartialOrder _≈_ _<_
  <-isStrictTotalOrder-≈   : IsStrictTotalOrder _≈_ _<_
  <-strictPartialOrder-≈   : StrictPartialOrder 0ℓ 0ℓ 0ℓ
  ```

* Added new functions to `Data.Rational.Base`:
  ```agda
  mkℚ+   : ∀ n d → .{d≢0 : d ≢0} → .(Coprime n d) → ℚ
  toℚᵘ   : ℚ → ℚᵘ
  fromℚᵘ : ℚᵘ → ℚ
  ```

* Added new proofs to `Data.Rational.Properties`:
  ```agda
  mkℚ-cong          : n₁ ≡ n₂ → d₁ ≡ d₂ → mkℚ n₁ d₁ c₁ ≡ mkℚ n₂ d₂ c₂
  mkℚ+-cong         : n₁ ≡ n₂ → d₁ ≡ d₂ → mkℚ+ n₁ d₁ c₁ ≡ mkℚ+ n₂ d₂ c₂
  normalize-coprime : .(c : Coprime n (suc d-1)) → normalize n (suc d-1) ≡ mkℚ (+ n) d-1 c

  ↥-mkℚ+            : ↥ (mkℚ+ n d c)                      ≡ + n
  ↧-mkℚ+            : ↧ (mkℚ+ n d c)                      ≡ + d
  ↥-neg             : ↥ (- p)                             ≡ - (↥ p)
  ↧-neg             : ↧ (- p)                             ≡ ↧ p
  ↥-normalise       : ↥ (normalize i n) * gcd (+ i) (+ n) ≡ + i
  ↧-normalise       : ↧ (normalize i n) * gcd (+ i) (+ n) ≡ + n
  ↥-/               : ↥ (i / n)         * gcd i (+ n)     ≡ i
  ↧-/               : ↧ (i / n)         * gcd i (+ n)     ≡ + n
  ↥-+               : ↥ (p + q)         * gcd (...) (...) ≡ ↥ p * ↧ q ℤ.+ ↥ q * ↧ p
  ↧-+               : ↧ (p + q)         * gcd (...) (...) ≡ ↧ p * ↧ q

  ↥p/↧p≡p           : ↥ p / ↧ₙ p ≡ p
  0/n≡0             : 0ℤ / n ≡ 0ℚ

  toℚᵘ-cong         : toℚᵘ Preserves _≡_ ⟶ _≃ᵘ_
  toℚᵘ-injective    : Injective _≡_ _≃ᵘ_ toℚᵘ
  fromℚᵘ-toℚᵘ       : fromℚᵘ (toℚᵘ p) ≡ p

  toℚᵘ-homo-+                : Homomorphic₂ toℚᵘ _+_ ℚᵘ._+_
  toℚᵘ-+-isRawMagmaMorphism  : IsRawMagmaMorphism +-rawMagma ℚᵘ.+-rawMagma toℚᵘ
  toℚᵘ-+-isRawMonoidMorphism : IsRawMonoidMorphism +-rawMonoid ℚᵘ.+-rawMonoid toℚᵘ

  +-assoc                    : Associative _+_
  +-comm                     : Commutative _+_
  +-identityˡ                : LeftIdentity 0ℚ _+_
  +-identityʳ                : RightIdentity 0ℚ _+_
  +-identity                 : Identity 0ℚ _+_
  +-isMagma                  : IsMagma _+_
  +-isSemigroup              : IsSemigroup _+_
  +-0-isMonoid               : IsMonoid _+_ 0ℚ
  +-0-isCommutativeMonoid    : IsCommutativeMonoid _+_ 0ℚ
  +-rawMagma                 : RawMagma 0ℓ 0ℓ
  +-rawMonoid                : RawMonoid 0ℓ 0ℓ
  +-magma                    : Magma 0ℓ 0ℓ
  +-semigroup                : Semigroup 0ℓ 0ℓ
  +-0-monoid                 : Monoid 0ℓ 0ℓ
  +-0-commutativeMonoid      : CommutativeMonoid 0ℓ 0ℓ
  ```

* Added new functions to `Data.Sum.Base`:
  ```agda
  fromInj₁ : (B → A) → A ⊎ B → A
  fromInj₂ : (A → B) → A ⊎ B → B
  ```

* Added new definition to `Data.These.Properties`:
  ```agda
  these-injective : these x a ≡ these y b → x ≡ y × a ≡ b
  ```

* Added new definition to `Data.Vec.Relation.Binary.Pointwise.Inductive`:
  ```agda
  uncons : Pointwise _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y × Pointwise _∼_ xs ys
  ```

* Added new definition to `Data.Vec.Relation.Unary.All`:
  ```agda
  uncons : All P (x ∷ xs) → P x × All P xs
  ```

* Added new functions to `Level`.
  ```agda
  levelOfType : ∀ {a} → Set a → Level
  levelOfTerm : ∀ {a} {A : Set a} → A → Level
  ```

* Added new proofs to `Relation.Binary.PropositionalEquality`:
  ```agda
  isMagma : (_∙_ : Op₂ A) → IsMagma _≡_ _∙_
  magma   : (_∙_ : Op₂ A) → Magma a a
  ```

* Added new definition to `Relation.Binary.Structures`:
  ```agda
  record IsPartialEquivalence (_≈_ : Rel A ℓ) : Set (a ⊔ ℓ)
  ```

* Added new definition to `Relation.Binary.Bundles`:
  ```agda
  record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ))
  ```

* Added new proofs to `Relation.Binary.Construct.NonStrictToStrict`:
  ```agda
  <⇒≉   : x < y → x ≉ y
  ≤∧≉⇒< : x ≤ y → x ≉ y → x < y
  <⇒≱   : Antisymmetric _≈_ _≤_ → ∀ {x y} → x < y → ¬ (y ≤ x)
  ≤⇒≯   : Antisymmetric _≈_ _≤_ → ∀ {x y} → x ≤ y → ¬ (y < x)
  ≰⇒>   : Symmetric _≈_ → (_≈_ ⇒ _≤_) → Total _≤_ → ∀ {x y} → ¬ (x ≤ y) → y < x
  ≮⇒≥   : Symmetric _≈_ → Decidable _≈_ → _≈_ ⇒ _≤_ → Total _≤_ → ∀ {x y} → ¬ (x < y) → y ≤ x
  ```

* Each of the following modules now re-export relevant proofs and relations from the previous modules in the list.
  ```
  Relation.Binary.Properties.Preorder
  Relation.Binary.Properties.Poset
  Relation.Binary.Properties.TotalOrder
  Relation.Binary.Properties.DecTotalOrder
  ```

* Added new relations and proofs to `Relation.Binary.Properties.Poset`:
  ```agda
  x ≥ y = y ≤ x
  x < y = ¬ (y ≈ x)

  <⇒≉   : x < y → x ≉ y
  ≤∧≉⇒< : x ≤ y → x ≉ y → x < y
  <⇒≱   : x < y → ¬ (y ≤ x)
  ≤⇒≯   : x ≤ y → ¬ (y < x)
  ```

* Added new proof to `Relation.Binary.Properties.TotalOrder`:
  ```agda
  ≰⇒> : ¬ (x ≤ y) → y < x
  ```

* Added new proof to `Relation.Binary.Properties.DecTotalOrder`:
  ```agda
  ≮⇒≥ : ¬ (x < y) → y ≤ x
  ```

* Added new proof to `Relation.Binary.PropositionalEquality`:
  ```agda
  isDecEquivalence : Decidable _≡_ → IsDecEquivalence _≡_
  ```

* Added new definitions to `Relation.Nary`:
  ```agda
  apply⊤ₙ     : Π[ R ] → (vs : Product⊤ n as) → uncurry⊤ₙ n R vs
  applyₙ      : Π[ R ] → (vs : Product n as)  → uncurry⊤ₙ n R (toProduct⊤ n vs)
  iapply⊤ₙ    : ∀[ R ] → {vs : Product⊤ n as} → uncurry⊤ₙ n R vs
  iapplyₙ     : ∀[ R ] → {vs : Product n as}  → uncurry⊤ₙ n R (toProduct⊤ n vs)

  Decidable   : as ⇉ Set r → Set (r ⊔ ⨆ n ls)
  ⌊_⌋         : Decidable R → as ⇉ Set r
  fromWitness : (R : as ⇉ Set r) (R? : Decidable R) → ∀[ ⌊ R? ⌋ ⇒ R ]
  toWitness   : (R : as ⇉ Set r) (R? : Decidable R) → ∀[ R ⇒ ⌊ R? ⌋ ]
  ```

* Added new definitions to `Relation.Unary`:
  ```agda
  ⌊_⌋ : {P : Pred A ℓ} → Decidable P → Pred A ℓ
  ```

* Added new definitions to `Relation.Binary.Construct.Closure.Reflexive.Properties`:
  ```agda
  fromSum :  a ≡ b ⊎ a ~ b  → Refl _~_ a b
  toSum   :  Refl _~_ a b   → a ≡ b ⊎ a ~ b
  ⊎⇔Refl  : (a ≡ b ⊎ a ~ b) ⇔ Refl _~_ a b
  ```

* Added new definitions to `Relation.Nullary.Decidable`:
  ```agda
  dec-true  : (p? : Dec P) →   P → does p? ≡ true
  dec-false : (p? : Dec P) → ¬ P → does p? ≡ false
  ```

* Added new definition to `Relation.Nullary.Implication`:
  ```agda
  _→-reflects_ : Reflects P bp → Reflects Q bq → Reflects (P → Q) (not bp ∨ bq)
  ```

* Added new definition to `Relation.Nullary.Negation`:
  ```agda
  ¬-reflects : Reflects P b → Reflects (¬ P) (not b)
  ```

* Added new definition to `Relation.Nullary.Product`:
  ```agda
  _×-reflects_ : Reflects P bp → Reflects Q bq → Reflects (P × Q) (bp ∧ bq)
  ```

* Added new definition to `Relation.Nullary.Sum`:
  ```agda
  _⊎-reflects_ : Reflects P bp → Reflects Q bq → Reflects (P ⊎ Q) (bp ∨ bq)
  ```

* The module `Size` now re-exports the built-in function:
  ```agda
  _⊔ˢ_ : Size → Size → Size
  ```