Version 2.1
===========
The library has been tested using Agda 2.6.4.3.
Highlights
----------
* The size of the dependency graph for many modules has been
reduced. This may lead to speed ups for first-time loading of some
modules.
* Added bindings for file handles in `IO.Handle`.
* Added bindings for random number generation in `System.Random`
* Added support for 8-bit words and bytestrings in `Data.Word8` and `Data.ByteString`.
Bug-fixes
---------
* Fixed type of `toList-replicate` in `Data.Vec.Properties`, where `replicate`
was mistakenly applied to the level of the type `A` instead of the
variable `x` of type `A`.
* Module `Data.List.Relation.Ternary.Appending.Setoid.Properties` no longer
incorrectly publicly exports the `Setoid` module under the alias `S`.
* Removed unbound parameter from `length-alignWith`,
`alignWith-map` and `map-alignWith` in `Data.List.Properties`.
Non-backwards compatible changes
--------------------------------
* The recently added modules and (therefore their contents) in:
```agda
Algebra.Module.Morphism.Structures
Algebra.Module.Morphism.Construct.Composition
Algebra.Module.Morphism.Construct.Identity
```
have been changed so they are now parametrized by _raw_ bundles rather
than lawful bundles.
This is in line with other modules that define morphisms.
As a result many of the `Composition` lemmas now take a proof of
transitivity and the `Identity` lemmas now take a proof of reflexivity.
* The module `IO.Primitive` was moved to `IO.Primitive.Core`.
Minor improvements
------------------
* The definition of the `Pointwise` relational combinator in
`Data.Product.Relation.Binary.Pointwise.NonDependent.Pointwise`
has been generalised to take heterogeneous arguments in `REL`.
* The structures `IsSemilattice` and `IsBoundedSemilattice` in
`Algebra.Lattice.Structures` have been redefined as aliases of
`IsCommutativeBand` and `IsIdempotentMonoid` in `Algebra.Structures`.
Deprecated modules
------------------
* All modules in the `Data.Word` hierarchy have been deprecated in favour
of their newly introduced counterparts in `Data.Word64`.
* The module `Data.List.Relation.Binary.Sublist.Propositional.Disjoint`
has been deprecated in favour of `Data.List.Relation.Binary.Sublist.Propositional.Slice`.
* The modules
```
Function.Endomorphism.Propositional
Function.Endomorphism.Setoid
```
that used the old `Function` hierarchy have been deprecated in favour of:
```
Function.Endo.Propositional
Function.Endo.Setoid
```
Deprecated names
----------------
* In `Algebra.Properties.Semiring.Mult`:
```agda
1×-identityʳ ↦ ×-homo-1
```
* In `Algebra.Structures.IsGroup`:
```agda
_-_ ↦ _//_
```
* In `Algebra.Structures.Biased`:
```agda
IsRing* ↦ Algebra.Structures.IsRing
isRing* ↦ Algebra.Structures.isRing
```
* In `Data.Float.Base`:
```agda
toWord ↦ toWord64
```
* In `Data.Float.Properties`:
```agda
toWord-injective ↦ toWord64-injective
```
* In `Data.List.Base`:
```agda
scanr ↦ Data.List.Scans.Base.scanr
scanl ↦ Data.List.Scans.Base.scanl
```
* In `Data.List.Properties`:
```agda
scanr-defn ↦ Data.List.Scans.Properties.scanr-defn
scanl-defn ↦ Data.List.Scans.Properties.scanl-defn
```
* In `Data.List.Relation.Unary.All.Properties`:
```agda
map-compose ↦ map-∘
```
* In `Data.Maybe.Base`:
```agda
decToMaybe ↦ Relation.Nullary.Decidable.Core.dec⇒maybe
```
* In `Data.Nat.Base`: the following pattern synonyms and definitions are all
deprecated in favour of direct pattern matching on `Algebra.Definitions.RawMagma._∣ˡ_._,_`
```agda
pattern less-than-or-equal {k} eq = k , eq
pattern ≤″-offset k = k , refl
pattern <″-offset k = k , refl
s≤″s⁻¹
```
* In `Data.Nat.Divisibility.Core`:
```agda
*-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣
```
* In `Data.Sum`:
```agda
fromDec ↦ Relation.Nullary.Decidable.Core.toSum
toDec ↦ Relation.Nullary.Decidable.Core.fromSum
```
* In `IO.Base`:
```agda
untilRight ↦ untilInj₂
```
New modules
-----------
* Pointwise lifting of algebraic structures `IsX` and bundles `X` from
carrier set `C` to function space `A → C`:
```
Algebra.Construct.Pointwise
```
* Raw bundles for module-like algebraic structures:
```
Algebra.Module.Bundles.Raw
```
* Nagata's construction of the "idealization of a module":
```agda
Algebra.Module.Construct.Idealization
```
* The unique morphism from the initial, resp. terminal, algebra:
```agda
Algebra.Morphism.Construct.Initial
Algebra.Morphism.Construct.Terminal
```
* Bytestrings and builders:
```agda
Data.Bytestring.Base
Data.Bytestring.Builder.Base
Data.Bytestring.Builder.Primitive
Data.Bytestring.IO
Data.Bytestring.IO.Primitive
Data.Bytestring.Primitive
```
* Pointwise and equality relations over indexed containers:
```agda
Data.Container.Indexed.Relation.Binary.Pointwise
Data.Container.Indexed.Relation.Binary.Pointwise.Properties
Data.Container.Indexed.Relation.Binary.Equality.Setoid
```
* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties:
```
Data.List.Scans.Base
Data.List.Scans.Properties
```
* Various show modules for lists and vector types:
```agda
Data.List.Show
Data.Vec.Show
Data.Vec.Bounded.Show
```
* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid):
```
Data.List.Relation.Binary.Equality.Setoid.Properties
```
* Decidability for the subset relation on lists:
```agda
Data.List.Relation.Binary.Subset.DecSetoid (_⊆?_)
Data.List.Relation.Binary.Subset.DecPropositional
```
* Decidability for the disjoint relation on lists:
```agda
Data.List.Relation.Binary.Disjoint.DecSetoid (disjoint?)
Data.List.Relation.Binary.Disjoint.DecPropositional
```
* Prime factorisation of natural numbers.
```agda
Data.Nat.Primality.Factorisation
```
* Permutations of vectors as functions:
```agda
Data.Vec.Functional.Relation.Binary.Permutation
Data.Vec.Functional.Relation.Binary.Permutation.Properties
```
* A type of bytes:
```agda
Data.Word8.Primitive
Data.Word8.Base
Data.Word8.Literals
Data.Word8.Show
```
* Word64 literals and bit-based functions:
```agda
Data.Word64.Literals
Data.Word64.Unsafe
Data.Word64.Show
```
* Pointwise equality over functions
```
Function.Relation.Binary.Equality`
```
* Consequences of 'infinite descent' for (accessible elements of) well-founded relations:
```agda
Induction.InfiniteDescent
```
* New IO primitives to handle buffering
```agda
IO.Primitive.Handle
IO.Handle
```
* Symmetric interior of a binary relation
```
Relation.Binary.Construct.Interior.Symmetric
```
* Properties of `Setoid`s with decidable equality relation:
```
Relation.Binary.Properties.DecSetoid
```
* Collection of results about recomputability in
```agda
Relation.Nullary.Recomputable
```
with the main definition `Recomputable` exported publicly from `Relation.Nullary`.
* New bindings to random numbers:
```agda
System.Random.Primitive
System.Random
```
Additions to existing modules
-----------------------------
* Added new definitions in `Algebra.Bundles`:
```agda
record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ))
record CommutativeBand c ℓ : Set (suc (c ⊔ ℓ))
record IdempotentMonoid c ℓ : Set (suc (c ⊔ ℓ))
```
and additional manifest fields for sub-bundles arising from these in:
```agda
IdempotentCommutativeMonoid
IdempotentSemiring
```
* Added new definition in `Algebra.Bundles.Raw`
```agda
record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ))
```
* Added new proofs in `Algebra.Construct.Terminal`:
```agda
rawNearSemiring : RawNearSemiring c ℓ
nearSemiring : NearSemiring c ℓ
```
* In `Algebra.Module.Bundles`, raw bundles are now re-exported and bundles
consistently expose their raw counterparts.
* Added proofs in `Algebra.Module.Construct.DirectProduct`:
```agda
rawLeftSemimodule : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawLeftModule : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawRightModule : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawBisemimodule : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawBimodule : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawSemimodule : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
rawModule : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
```
* Added proofs in `Algebra.Module.Construct.TensorUnit`:
```agda
rawLeftSemimodule : RawLeftSemimodule _ c ℓ
rawLeftModule : RawLeftModule _ c ℓ
rawRightSemimodule : RawRightSemimodule _ c ℓ
rawRightModule : RawRightModule _ c ℓ
rawBisemimodule : RawBisemimodule _ _ c ℓ
rawBimodule : RawBimodule _ _ c ℓ
rawSemimodule : RawSemimodule _ c ℓ
rawModule : RawModule _ c ℓ
```
* Added proofs in `Algebra.Module.Construct.Zero`:
```agda
rawLeftSemimodule : RawLeftSemimodule R c ℓ
rawLeftModule : RawLeftModule R c ℓ
rawRightSemimodule : RawRightSemimodule R c ℓ
rawRightModule : RawRightModule R c ℓ
rawBisemimodule : RawBisemimodule R c ℓ
rawBimodule : RawBimodule R c ℓ
rawSemimodule : RawSemimodule R c ℓ
rawModule : RawModule R c ℓ
```
* Added definitions in `Algebra.Morphism.Structures`:
```agda
record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
record IsSuccessorSetIsomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
IsSemigroupHomomorphism : (A → B) → Set _
IsSemigroupMonomorphism : (A → B) → Set _
IsSemigroupIsomorphism : (A → B) → Set _
```
* Added proof in `Algebra.Properties.AbelianGroup`:
```
⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x
```
* Added proofs in `Algebra.Properties.Group`:
```agda
isQuasigroup : IsQuasigroup _∙_ _\\_ _//_
quasigroup : Quasigroup _ _
isLoop : IsLoop _∙_ _\\_ _//_ ε
loop : Loop _ _
\\-leftDividesˡ : LeftDividesˡ _∙_ _\\_
\\-leftDividesʳ : LeftDividesʳ _∙_ _\\_
\\-leftDivides : LeftDivides _∙_ _\\_
//-rightDividesˡ : RightDividesˡ _∙_ _//_
//-rightDividesʳ : RightDividesʳ _∙_ _//_
//-rightDivides : RightDivides _∙_ _//_
⁻¹-selfInverse : SelfInverse _⁻¹
x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y
x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε
\\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x
⁻¹-anti-homo-// : (x // y) ⁻¹ ≈ y // x
⁻¹-anti-homo-\\ : (x \\ y) ⁻¹ ≈ y \\ x
```
* Added new proofs in `Algebra.Properties.Loop`:
```agda
identityˡ-unique : x ∙ y ≈ y → x ≈ ε
identityʳ-unique : x ∙ y ≈ x → y ≈ ε
identity-unique : Identity x _∙_ → x ≈ ε
```
* Added new proofs in `Algebra.Properties.Monoid.Mult`:
```agda
×-homo-0 : 0 × x ≈ 0#
×-homo-1 : 1 × x ≈ x
```
* Added new proofs in `Algebra.Properties.Semiring.Mult`:
```agda
×-homo-0# : 0 × x ≈ 0# * x
×-homo-1# : 1 × x ≈ 1# * x
idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
```
* Added new definitions to `Algebra.Structures`:
```agda
record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _
record IsCommutativeBand (∙ : Op₂ A) : Set _
record IsIdempotentMonoid (∙ : Op₂ A) (ε : A) : Set _
```
* Added new definitions in `IsGroup` record in `Algebra.Structures`:
```agda
x // y = x ∙ (y ⁻¹)
x \\ y = (x ⁻¹) ∙ y
```
* In `Algebra.Structures` added new proof to `IsCancellativeCommutativeSemiring` record:
```agda
*-cancelʳ-nonZero : AlmostRightCancellative 0# *
```
* In `Data.Bool.Show`:
```agda
showBit : Bool → Char
```
* In `Data.Container.Indexed.Core`:
```agda
Subtrees o c = (r : Response c) → X (next c r)
```
* In `Data.Empty`:
```agda
⊥-elim-irr : .⊥ → Whatever
```
* In `Data.Fin.Properties`:
```agda
nonZeroIndex : Fin n → ℕ.NonZero n
```
* In `Data.Float.Base`:
```agda
_≤_ : Rel Float _
```
* In `Data.Integer.Divisibility` introduced `divides` as an explicit pattern synonym
```agda
pattern divides k eq = Data.Nat.Divisibility.divides k eq
```
* In `Data.Integer.Properties`:
```agda
◃-nonZero : .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
sign-* : .{{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j
i*j≢0 : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
```
* In `Data.List.Base` added two new functions:
```agda
Inits.tail : List A → List (List A)
Tails.tail : List A → List (List A)
```
and redefined `inits` and `tails` in terms of them.
* In `Data.List.Membership.Propositional.Properties.Core`:
```agda
find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p
∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
```
* In `Data.List.Membership.Setoid.Properties`:
```agda
reverse⁺ : x ∈ xs → x ∈ reverse xs
reverse⁻ : x ∈ reverse xs → x ∈ xs
```
* In `Data.List.Properties`:
```agda
length-catMaybes : length (catMaybes xs) ≤ length xs
applyUpTo-∷ʳ : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
applyDownFrom-∷ʳ : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
upTo-∷ʳ : upTo n ∷ʳ n ≡ upTo (suc n)
downFrom-∷ʳ : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
reverse-selfInverse : SelfInverse {A = List A} _≡_ reverse
reverse-applyUpTo : reverse (applyUpTo f n) ≡ applyDownFrom f n
reverse-upTo : reverse (upTo n) ≡ downFrom n
reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n
reverse-downFrom : reverse (downFrom n) ≡ upTo n
mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g)
map-mapMaybe : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f)
align-map : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys)
zip-map : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys)
unzipWith-map : unzipWith f ∘ map g ≗ unzipWith (f ∘ g)
map-unzipWith : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f)
unzip-map : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip
splitAt-map : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n
uncons-map : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons
last-map : last ∘ map f ≗ map f ∘ last
tail-map : tail ∘ map f ≗ map (map f) ∘ tail
mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g
zipWith-cong : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as
unzipWith-cong : f ≗ g → unzipWith f ≗ unzipWith g
foldl-cong : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x
alignWith-flip : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs
alignWith-comm : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs
align-flip : align xs ys ≡ map swap (align ys xs)
zip-flip : zip xs ys ≡ map swap (zip ys xs)
unzipWith-swap : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f
unzip-swap : unzip ∘ map swap ≗ swap ∘ unzip
take-take : take n (take m xs) ≡ take (n ⊓ m) xs
take-drop : take n (drop m xs) ≡ drop m (take (m + n) xs)
zip-unzip : uncurry′ zip ∘ unzip ≗ id
unzipWith-zipWith : f ∘ uncurry′ g ≗ id →
length xs ≡ length ys →
unzipWith f (zipWith g xs ys) ≡ (xs , ys)
unzip-zip : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys)
mapMaybe-++ : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys
unzipWith-++ : unzipWith f (xs ++ ys) ≡
zip _++_ _++_ (unzipWith f xs) (unzipWith f ys)
catMaybes-concatMap : catMaybes ≗ concatMap fromMaybe
catMaybes-++ : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys
map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
Any-catMaybes⁺ : Any (M.Any P) xs → Any P (catMaybes xs)
mapMaybeIsInj₁∘mapInj₁ : mapMaybe isInj₁ (map inj₁ xs) ≡ xs
mapMaybeIsInj₁∘mapInj₂ : mapMaybe isInj₁ (map inj₂ xs) ≡ []
mapMaybeIsInj₂∘mapInj₂ : mapMaybe isInj₂ (map inj₂ xs) ≡ xs
mapMaybeIsInj₂∘mapInj₁ : mapMaybe isInj₂ (map inj₁ xs) ≡ []
```
* In `Data.List.Relation.Binary.Pointwise.Base`:
```agda
unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S)
```
* In `Data.List.Relation.Binary.Sublist.Setoid`:
```agda
⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ
```
* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
```agda
⊆-trans-idˡ : (trans-reflˡ : ∀ {x y} (p : x ≈ y) → trans ≈-refl p ≡ p) →
(pxs : xs ⊆ ys) → ⊆-trans ⊆-refl pxs ≡ pxs
⊆-trans-idʳ : (trans-reflʳ : ∀ {x y} (p : x ≈ y) → trans p ≈-refl ≡ p) →
(pxs : xs ⊆ ys) → ⊆-trans pxs ⊆-refl ≡ pxs
⊆-trans-assoc : (≈-assoc : ∀ {w x y z} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z) →
trans p (trans q r) ≡ trans (trans p q) r) →
(ps : as ⊆ bs) (qs : bs ⊆ cs) (rs : cs ⊆ ds) →
⊆-trans ps (⊆-trans qs rs) ≡ ⊆-trans (⊆-trans ps qs) rs
```
* In `Data.List.Relation.Unary.All`:
```agda
universal-U : Universal (All U)
```
* In `Data.List.Relation.Unary.All.Properties`:
```agda
All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
Any-catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs)
```
* In `Data.List.Relation.Unary.AllPairs.Properties`:
```agda
catMaybes⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs)
tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f)
```
* In `Data.List.Relation.Unary.Any.Properties`:
```agda
map-cong : (f g : P ⋐ Q) → (∀ {x} (p : P x) → f p ≡ g p) →
(p : Any P xs) → Any.map f p ≡ Any.map g p
```
* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
```agda
product-↭ : product Preserves _↭_ ⟶ _≡_
catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
```
* Added new proofs to `Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe`:
```agda
catMaybes-↭ : xs ↭ ys → catMaybes xs ↭ catMaybes ys
mapMaybe-↭ : xs ↭ ys → mapMaybe f xs ↭ mapMaybe f ys
```
* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
```agda
map⁺ : f Preserves _≈_ ⟶ _≈′_ → as ⊆ bs → map f as ⊆′ map f bs
reverse-selfAdjoint : as ⊆ reverse bs → reverse as ⊆ bs
reverse⁺ : as ⊆ bs → reverse as ⊆ reverse bs
reverse⁻ : reverse as ⊆ reverse bs → as ⊆ bs
```
* Added new proofs to `Data.List.Relation.Binary.Sublist.Propositional.Slice`:
```agda
⊆-upper-bound-is-cospan : (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → IsCospan (⊆-upper-bound τ₁ τ₂)
⊆-upper-bound-cospan : (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → Cospan τ₁ τ₂
```
* In `Data.List.Relation.Ternary.Appending.Setoid.Properties`:
```agda
through→ : ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs →
∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs
through← : ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs →
∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs
assoc→ : ∃[ xs ] Appending as bs xs × Appending xs cs ds →
∃[ ys ] Appending bs cs ys × Appending as ys ds
```
* In `Data.List.Relation.Ternary.Appending.Properties`:
```agda
through→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) →
∃[ xs ] Pointwise U as xs × Appending V R xs bs cs →
∃[ ys ] Appending W S as bs ys × Pointwise T ys cs
through← : ((R ; S) ⇒ T) → ((U ; S) ⇒ (V ; W)) →
∃[ ys ] Appending U R as bs ys × Pointwise S ys cs →
∃[ xs ] Pointwise V as xs × Appending W T xs bs cs
assoc→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) → ((Y ; V) ⇒ X) →
∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds →
∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds
assoc← : ((S ; T) ⇒ R) → ((W ; T) ⇒ (U ; V)) → (X ⇒ (Y ; V)) →
∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds →
∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds
```
* In `Data.List.NonEmpty.Base`:
```agda
inits : List A → List⁺ (List A)
tails : List A → List⁺ (List A)
```
* In `Data.List.NonEmpty.Properties`:
```agda
toList-inits : toList ∘ List⁺.inits ≗ List.inits
toList-tails : toList ∘ List⁺.tails ≗ List.tails
```
* In `Data.Maybe.Relation.Binary.Pointwise`:
```agda
pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
```
* In `Data.Nat.Divisibility`:
```agda
quotient≢0 : m ∣ n → .{{NonZero n}} → NonZero quotient
m∣n⇒n≡quotient*m : m ∣ n → n ≡ quotient * m
m∣n⇒n≡m*quotient : m ∣ n → n ≡ m * quotient
quotient-∣ : m ∣ n → quotient ∣ n
quotient>1 : m ∣ n → m < n → 1 < quotient
quotient-< : m ∣ n → .{{NonTrivial m}} → .{{NonZero n}} → quotient < n
n/m≡quotient : m ∣ n → .{{_ : NonZero m}} → n / m ≡ quotient
m/n≡0⇒m<n : .{{_ : NonZero n}} → m / n ≡ 0 → m < n
m/n≢0⇒n≤m : .{{_ : NonZero n}} → m / n ≢ 0 → n ≤ m
nonZeroDivisor : DivMod dividend divisor → NonZero divisor
```
* Added new proofs to `Data.Nat.Primality`:
```agda
rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n
productOfPrimes≢0 : All Prime as → NonZero (product as)
productOfPrimes≥1 : All Prime as → product as ≥ 1
```
* Added new proofs in `Data.Nat.Properties`:
```agda
m≤n+o⇒m∸n≤o : m ≤ n + o → m ∸ n ≤ o
m<n+o⇒m∸n<o : .{{NonZero o}} → m < n + o → m ∸ n < o
pred-cancel-≤ : pred m ≤ pred n → (m ≡ 1 × n ≡ 0) ⊎ m ≤ n
pred-cancel-< : pred m < pred n → m < n
pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
<⇒<″ : _<_ ⇒ _<″_
m≤n⇒∃[o]m+o≡n : .(m ≤ n) → ∃ λ k → m + k ≡ n
guarded-∸≗∸ : .(m≤n : m ≤ n) → let k , _ = m≤n⇒∃[o]m+o≡n m≤n in k ≡ n ∸ m
```
* Added some very-dependent map and zipWith to `Data.Product`.
```agda
map-Σ : {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} →
(f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) →
((x , y) : Σ A P) → Σ (B x) (Q y)
map-Σ′ : {B : A → Set b} {P : Set p} {Q : P → Set q} →
(f : (x : A) → B x) → ((x : P) → Q x) → ((x , y) : A × P) → B x × Q y
zipWith : {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s}
(_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) →
(_*_ : (x : C) → (y : R x) → S x y) →
((a , p) : Σ A P) → ((b , q) : Σ B Q) →
S (a ∙ b) (p ∘ q)
```
* In `Data.Rational.Properties`:
```agda
1≢0 : 1ℚ ≢ 0ℚ
#⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q)
invertible⇒# : Invertible 1ℚ _*_ (p - q) → p ≢ q
isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ
heytingField : HeytingField 0ℓ 0ℓ 0ℓ
```
* Added new functions in `Data.String.Base`:
```agda
map : (Char → Char) → String → String
between : String → String → String → String
```
* Added new functions in `Data.Vec.Bounded.Base`:
```agda
isBounded : (as : Vec≤ A n) → Vec≤.length as ≤ n
toVec : (as : Vec≤ A n) → Vec A (Vec≤.length as)
```
* In `Data.Word64.Base`:
```agda
_≤_ : Rel Word64 zero
show : Word64 → String
```
* In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can
be used infix.
* Re-exported new types and functions in `IO`:
```agda
BufferMode : Set
noBuffering : BufferMode
lineBuffering : BufferMode
blockBuffering : Maybe ℕ → BufferMode
Handle : Set
stdin : Handle
stdout : Handle
stderr : Handle
hSetBuffering : Handle → BufferMode → IO ⊤
hGetBuffering : Handle → IO BufferMode
hFlush : Handle → IO ⊤
```
* Added new functions in `IO.Base`:
```agda
whenInj₂ : E ⊎ A → (A → IO ⊤) → IO ⊤
forever : IO ⊤ → IO ⊤
```
* In `IO.Primitive.Core`:
```agda
_>>_ : IO A → IO B → IO B
```
* Added new definition in `Relation.Binary.Construct.Closure.Transitive`
```agda
transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_
```
* Added new proofs in `Relation.Binary.Construct.Composition`:
```agda
transitive⇒≈;≈⊆≈ : Transitive ≈ → (≈ ; ≈) ⇒ ≈
```
* Added new definitions in `Relation.Binary.Definitions`
```agda
Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y)
Empty _∼_ = ∀ {x y} → ¬ (x ∼ y)
```
* Added new proofs in `Relation.Binary.Properties.Setoid`:
```agda
≉-irrefl : Irreflexive _≈_ _≉_
≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_
≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_
```
* Added new definitions in `Relation.Nullary`
```agda
Recomputable : Set _
WeaklyDecidable : Set _
```
* Added new proof in `Relation.Nullary.Decidable`:
```agda
⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
```
* Added new definitions and proofs in `Relation.Nullary.Decidable.Core`:
```agda
dec⇒maybe : Dec A → Maybe A
recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
toSum : Dec A → A ⊎ ¬ A
fromSum : A ⊎ ¬ A → Dec A
```
* Added new definitions in `Relation.Nullary.Negation.Core`:
```agda
contradiction-irr : .A → ¬ A → Whatever
```
* Added new definitions in `Relation.Nullary.Reflects`:
```agda
recompute : Reflects A b → Recomputable A
recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
```
* Added new definitions in `Relation.Unary`:
```agda
Stable : Pred A ℓ → Set _
WeaklyDecidable : Pred A ℓ → Set _
```
* Enhancements to `Tactic.Cong` - see `README.Tactic.Cong` for details.
- Provide a marker function, `⌞_⌟`, for user-guided anti-unification.
- Improved support for equalities between terms with instance arguments,
such as terms that contain `_/_` or `_%_`.