path: root/CHANGELOG/v0.15.md

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
  ```