jamesmckinna

[ refactor ] Exchange components of `Relation.Binary.Definitions._Respects₂_`

3

Fixes #2471 Lots of (trivial) knock-on viscosity: PR takes the opportunity to rename/refactor proofs in (hopefully!) helpful ways. Is this v2.x or v3.0, because `breaking`?

[ refactor ] Add equality as a parameter to `Algebra.Consequences.Base`

5

See [this comment](https://github.com/agda/agda-stdlib/issues/2502#issuecomment-2613113410) on issue #2502 . By analogy with `Algebra.Definitions` and `Algebra.Structures`... moreover `non-breaking`. Indeed, `Base` is only imported by `Algebra.Consequences.Setoid` (and by the now-deprecated module `Algebra.FunctionProperties.Consequences.Core`), so there...

[ refactor ] Redefine `Relation.Binary.Definitions.Adjoint`, plus knock-on `Function.Consequences`

1

Fixes #2581 .

[ refactor ] use `variable`s in `Algebra.Consequences.Base`

2

This lifts out the refactoring aspects of #2572 and should be merged first of the two. It also rectifies two bugs * use of deprecated names in `Data.Rational.Unnormalised.Properties` * changing...

Redefine `Algebra.Consequences.Setoid.wlog`

6

The trouble with [the definition](https://github.com/agda/agda-stdlib/blob/2bce915db17fc284c7ed7a13d91cffe7a058a1e1/src/Algebra/Consequences/Setoid.agda#L311-L325): ```agda ------------------------------------------------------------------------ -- Without Loss of Generality module _ {p} {P : Pred A p} (≈-subst : Substitutive _≈_ p) (∙-comm : Commutative _∙_) where...

Refactor `Algebra.Consequences.*`?

6

These modules are structured around: * `Base`, depending only on the underlying `Carrier` set `A`, whose properties make explicit a dependency on a(n equality) relation `_≈_ : Rel A ℓ`;...

Tidy up `Algebra.Definitions.RawMagma` (again), plus reconcile all the uses of `_,_` as a constructor

4

Variations on the theme of uncoupling from `Data.Product.Base`, lifted out from #2579 : cf. #207 * `bug`: we don't give fixities to the various uses of `_,_` as a constructor...

[ refactor ] Reconcile `Relation.Binary.Definitions.Adjoint` and `Function.Definitions.Inverse*`

5

Meditating on #2580 (and some other recent PRs, including those which touch `Function.*`), it's hard not to observe the following: * `Relation.Binary.Definitions.Adjoint` universally quantifies the product of two implications, rather...

```quote * the PR itself draws attention to the fact that `Symmetric _#_` is in fact a redundant part of the definition of `IsHeytingCommutativeRing`, so it *might* be worth having...

[ refactor ] Remove `sum` and `product` (and their properties) from `Data.List.*`

5

This is a long-standing legacy issue (cf. #1099 ) that causes problems esp. regarding: * the dependency graph: `Data.List.Base` and `Properties` need to import `Data.Nat.Divisibility` otherwise unnecessarily; also, how much...