mechvel

Deprecate old function hierarchy

9

I propose the following two backwards compatible additions. (1) To add to ``Function.Injection`` ``` InjectiveBy≡ : ∀ {a b} {A : Set a} {B : Set b} → (A →...

Big `Data.(Nat/Integer).Properties` wishlist

3

* [x] Add [`⊔-mono-≤`](http://agda.github.io/agda-stdlib/Data.Nat.Properties.html#32000) and friends * [ ] Make notations uniform for [`≤- n → m ≢ n` * [x] `m+suc[n]≡suc[m]+n : ∀ m n → m + suc...

generic Nonzero proposal

19

The master lib of April 28, 2020 has ``NonZero`` for Integer, ℚ and maybe for other special domains. I suggest to generalize this to ``IsNonzero : Pred Carrier _`` and...

Add `_≮_` and `_≰_` to bundles in the binary relation hierarchy.

4

In lib-1.3 I see ``_≉_`` in Setoid, but I do not find ``≰, ≮`` (I expect they to be defined via ``¬_``). I grepped for it in Relation.Binary, Relation.Binary.Construct, and...

`WellFounded` for lexicographic ordering on `Vector`.

1

Probably WellFounded does not hold for

A name for ``P x → P (f x)``

8

For ``P : Pred A _, f : A → A``, what is the standard library type definition for ``{x : A} → P x → P (f x)`` ?...

Proposal with `∣quot` and `∣eq` for `_∣_`

2

Algebra.Definitions.RawMagma defines ``` _∣_ : Rel A (a ⊔ ℓ) x ∣ y = ∃ λ q → (q ∙ x) ≈ y ``` (here I omit the upper index...

proposal to reorganize the divisibility relation ``_|_ ``

9

Matthew wrote > The discussion for how this stage of the changes should be laid out should > really be continued in an issue on Github. If you'd like to...

AlmostCancellative in Nat.Properties ?

2

lib-1.7 has a general notion AlmostLeft(Right)Cancellative, and it is used in `*-cancelˡ-nonZero` in `IsCancellativeCommutativeSemiring`. On the other hand `Nat.Properties` has the definitions of kind. ``` *-cancelʳ-≡ : ∀ m n...

Respects₂-generic ?

7

Relation.Binary.Core has ` _Respects₂_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _` And I introduce ```agda Respects₂gen :...