@@ -17,6 +17,17 @@ Bug-fixes
1717 the record constructors ` _,_ ` incorrectly had no declared fixity. They have been given
1818 the fixity ` infixr 4 _,_ ` , consistent with that of ` Data.Product.Base ` .
1919
20+ * In ` Data.Product.Function.Dependent.Setoid ` , ` left-inverse ` defined a
21+ ` RightInverse ` .
22+ This has been deprecated in favor or ` rightInverse ` , and a corrected (and
23+ correctly-named) function ` leftInverse ` has been added.
24+
25+ * The implementation of ` _IsRelatedTo_ ` in ` Relation.Binary.Reasoning.Base.Partial `
26+ has been modified to correctly support equational reasoning at the beginning and the end.
27+ The detail of this issue is described in [ #2677 ] ( https://github.com/agda/agda-stdlib/pull/2677 ) . Since the names of constructors
28+ of ` _IsRelatedTo_ ` are changed and the reduction behaviour of reasoning steps
29+ are changed, this modification is non-backwards compatible.
30+
2031Non-backwards compatible changes
2132--------------------------------
2233
@@ -134,6 +145,11 @@ Deprecated names
134145 product-↭ ↦ Data.Nat.ListAction.Properties.product-↭
135146```
136147
148+ * In ` Data.Product.Function.Dependent.Setoid ` :
149+ ``` agda
150+ left-inverse ↦ rightInverse
151+ ```
152+
137153New modules
138154-----------
139155
@@ -147,7 +163,11 @@ New modules
147163
148164* ` Data.List.Relation.Binary.Suffix.Propositional.Properties ` showing the equivalence to right divisibility induced by the list monoid.
149165
150- * ` Data.Sign.Show ` to show a sign
166+ * ` Data.Sign.Show ` to show a sign.
167+
168+ * ` Relation.Binary.Morphism.Construct.Product ` to plumb in the (categorical) product structure on ` RawSetoid ` .
169+
170+ * ` Relation.Binary.Properties.PartialSetoid ` to systematise properties of a PER
151171
152172Additions to existing modules
153173-----------------------------
@@ -219,17 +239,129 @@ Additions to existing modules
219239 ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
220240```
221241
242+ * In ` Data.Fin.Base ` :
243+ ``` agda
244+ _≰_ : Rel (Fin n) 0ℓ
245+ _≮_ : Rel (Fin n) 0ℓ
246+ ```
247+
248+ * In ` Data.Fin.Permutation ` :
249+ ``` agda
250+ cast-id : .(m ≡ n) → Permutation m n
251+ swap : Permutation m n → Permutation (suc (suc m)) (suc (suc n))
252+ ```
253+
254+ * In ` Data.Fin.Properties ` :
255+ ``` agda
256+ cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k
257+ ```
258+
259+ * In ` Data.Fin.Subset ` :
260+ ``` agda
261+ _⊇_ : Subset n → Subset n → Set
262+ _⊉_ : Subset n → Subset n → Set
263+ _⊃_ : Subset n → Subset n → Set
264+ _⊅_ : Subset n → Subset n → Set
265+
266+ ```
267+
268+ * In ` Data.Fin.Subset.Induction ` :
269+ ``` agda
270+ ⊃-Rec : RecStruct (Subset n) ℓ ℓ
271+ ⊃-wellFounded : WellFounded _⊃_
272+ ```
273+
274+ * In ` Data.Fin.Subset.Properties `
275+ ``` agda
276+ p⊆q⇒∁p⊇∁q : p ⊆ q → ∁ p ⊇ ∁ q
277+ ∁p⊆∁q⇒p⊇q : ∁ p ⊆ ∁ q → p ⊇ q
278+ p⊂q⇒∁p⊃∁q : p ⊂ q → ∁ p ⊃ ∁ q
279+ ∁p⊂∁q⇒p⊃q : ∁ p ⊂ ∁ q → p ⊃ q
280+ ```
281+
222282* In ` Data.List.Properties ` :
223283 ``` agda
284+ length-++-sucˡ : ∀ (x : A) (xs ys : List A) → length (x ∷ xs ++ ys) ≡ suc (length (xs ++ ys))
285+ length-++-sucʳ : ∀ (xs : List A) (y : A) (ys : List A) → length (xs ++ y ∷ ys) ≡ suc (length (xs ++ ys))
286+ length-++-comm : ∀ (xs ys : List A) → length (xs ++ ys) ≡ length (ys ++ xs)
287+ length-++-≤ˡ : ∀ (xs : List A) → length xs ≤ length (xs ++ ys)
288+ length-++-≤ʳ : ∀ (ys : List A) → length ys ≤ length (xs ++ ys)
224289 map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n
225290 map-applyDownFrom : ∀ (f : ℕ → A) (g : A → B) n → map g (applyDownFrom f n) ≡ applyDownFrom (g ∘ f) n
226291 map-upTo : ∀ (f : ℕ → A) n → map f (upTo n) ≡ applyUpTo f n
227292 map-downFrom : ∀ (f : ℕ → A) n → map f (downFrom n) ≡ applyDownFrom f n
228293```
229294
230- * In ` Data.List.Relation.Binary.Permutation.PropositionalProperties ` :
295+ * In ` Data.List.Relation.Binary.Permutation.Homogeneous ` :
296+ ``` agda
297+ onIndices : Permutation R xs ys → Fin.Permutation (length xs) (length ys)
298+ ```
299+
300+ * In ` Data.List.Relation.Binary.Permutation.Propositional ` :
301+ ``` agda
302+ ↭⇒↭ₛ′ : IsEquivalence _≈_ → _↭_ ⇒ _↭ₛ′_
303+ ```
304+
305+ * In ` Data.List.Relation.Binary.Permutation.Setoid.Properties ` :
306+ ``` agda
307+ xs↭ys⇒|xs|≡|ys| : xs ↭ ys → length xs ≡ length ys
308+ ¬x∷xs↭[] : ¬ (x ∷ xs ↭ [])
309+ onIndices-lookup : ∀ i → lookup xs i ≈ lookup ys (Inverse.to (onIndices xs↭ys) i)
310+ ```
311+
312+ * In ` Data.List.Relation.Binary.Permutation.Propositional.Properties ` :
231313 ``` agda
232314 filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
315+ ```
316+
317+ * In `Data.List.Relation.Binary.Pointwise.Properties`:
318+ ```agda
319+ lookup-cast : Pointwise R xs ys → .(∣xs∣≡∣ys∣ : length xs ≡ length ys) → ∀ i → R (lookup xs i) (lookup ys (cast ∣xs∣≡∣ys∣ i))
320+ ```
321+
322+ * In ` Data.List.NonEmpty.Properties ` :
323+ ``` agda
324+ ∷→∷⁺ : (x List.∷ xs) ≡ (y List.∷ ys) →
325+ (x List⁺.∷ xs) ≡ (y List⁺.∷ ys)
326+ ∷⁺→∷ : (x List⁺.∷ xs) ≡ (y List⁺.∷ ys) →
327+ (x List.∷ xs) ≡ (y List.∷ ys)
328+ length-⁺++⁺ : (xs ys : List⁺ A) → length (xs ⁺++⁺ ys) ≡ length xs + length ys
329+ length-⁺++⁺-comm : ∀ (xs ys : List⁺ A) → length (xs ⁺++⁺ ys) ≡ length (ys ⁺++⁺ xs)
330+ length-⁺++⁺-≤ˡ : (xs ys : List⁺ A) → length xs ≤ length (xs ⁺++⁺ ys)
331+ length-⁺++⁺-≤ʳ : (xs ys : List⁺ A) → length ys ≤ length (xs ⁺++⁺ ys)
332+ map-⁺++⁺ : ∀ (f : A → B) xs ys → map f (xs ⁺++⁺ ys) ≡ map f xs ⁺++⁺ map f ys
333+ ⁺++⁺-assoc : Associative _⁺++⁺_
334+ ⁺++⁺-cancelˡ : LeftCancellative _⁺++⁺_
335+ ⁺++⁺-cancelʳ : RightCancellative _⁺++⁺_
336+ ⁺++⁺-cancel : Cancellative _⁺++⁺_
337+ map-id : map id ≗ id {A = List⁺ A}
338+ ```
339+
340+ * In ` Data.Product.Function.Dependent.Propositional ` :
341+ ``` agda
342+ Σ-↪ : (I↪J : I ↪ J) → (∀ {j} → A (from I↪J j) ↪ B j) → Σ I A ↪ Σ J B
343+ ```
344+
345+ * In ` Data.Product.Function.Dependent.Setoid ` :
346+ ``` agda
347+ rightInverse :
348+ (I↪J : I ↪ J) →
349+ (∀ {j} → RightInverse (A atₛ (from I↪J j)) (B atₛ j)) →
350+ RightInverse (I ×ₛ A) (J ×ₛ B)
351+
352+ leftInverse :
353+ (I↩J : I ↩ J) →
354+ (∀ {i} → LeftInverse (A atₛ i) (B atₛ (to I↩J i))) →
355+ LeftInverse (I ×ₛ A) (J ×ₛ B)
356+ ```
357+
358+ * In ` Data.Vec.Relation.Binary.Pointwise.Inductive ` :
359+ ``` agda
360+ zipWith-assoc : Associative _∼_ f → Associative (Pointwise _∼_) (zipWith {n = n} f)
361+ zipWith-identityˡ: LeftIdentity _∼_ e f → LeftIdentity (Pointwise _∼_) (replicate n e) (zipWith f)
362+ zipWith-identityʳ: RightIdentity _∼_ e f → RightIdentity (Pointwise _∼_) (replicate n e) (zipWith f)
363+ zipWith-comm : Commutative _∼_ f → Commutative (Pointwise _∼_) (zipWith {n = n} f)
364+ zipWith-cong : Congruent₂ _∼_ f → Pointwise _∼_ ws xs → Pointwise _∼_ ys zs → Pointwise _∼_ (zipWith f ws ys) (zipWith f xs zs)
233365```
234366
235367* In ` Relation.Binary.Construct.Add.Infimum.Strict ` :
@@ -258,4 +390,28 @@ Additions to existing modules
258390 ⊥-sym : Symmetric _⊥_
259391 ≬⇒¬⊥ : _≬_ ⇒ (¬_ ∘₂ _⊥_)
260392 ⊥⇒¬≬ : _⊥_ ⇒ (¬_ ∘₂ _≬_)
393+
394+ * In `Relation.Nullary.Negation.Core`:
395+ ```agda
396+ contra-diagonal : (A → ¬ A) → ¬ A
397+ ```
398+
399+ * In ` Relation.Nullary.Reflects ` :
400+ ``` agda
401+ ⊤-reflects : Reflects (⊤ {a}) true
402+ ⊥-reflects : Reflects (⊥ {a}) false
403+
404+ * In `Data.List.Relation.Unary.AllPairs.Properties`:
405+ ```agda
406+ map⁻ : AllPairs R (map f xs) → AllPairs (R on f) xs
407+ ```
408+
409+ * In ` Data.List.Relation.Unary.Unique.Setoid.Properties ` :
410+ ``` agda
411+ map⁻ : Congruent _≈₁_ _≈₂_ f → Unique R (map f xs) → Unique S xs
412+ ```
413+
414+ * In ` Data.List.Relation.Unary.Unique.Propositional.Properties ` :
415+ ``` agda
416+ map⁻ : Unique (map f xs) → Unique xs
261417```
0 commit comments