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