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