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