Add a few algebraic structures missing from the Algebra.Construct.Pointwise

[bsaul]

This PR adds a few structures/bundles currently missing from Algebra.Construct.Pointwise, namely:

• isNearSemiring
• isSemiringWithoutOne
• isCommutativeSemiringWithoutOne
• isCommutativeSemiring
• isIdempotentSemiring
• isKleeneAlgebra
• isQuasiring
• isCommutativeRing

[jamesmckinna]

Bradley, thanks for mopping up the missing pieces of #2381 ! A nice first PR.

NB we'll need a CHANGELOG entry, and while we should #2557 begin again for v2.3 with a clean CHANGELOG rather than the v2.2 one currently in-place on master, the fact that this PR touches only one module should mean that your commits won't give rise to merge conflicts... so suggest you add those entries now?

[bsaul]

Bradley, thanks for mopping up the missing pieces of #2381 ! A nice first PR.

Thanks!

NB we'll need a CHANGELOG entry, and while we should #2557 begin again for v2.3 with a clean CHANGELOG rather than the v2.2 one currently in-place on master, the fact that this PR touches only one module should mean that your commits won't give rise to merge conflicts... so suggest you add those entries now?

To be clear, you'd like me to add something like the following?

Version 2.3-dev
===========

Additions to existing modules
-----------------------------

* In `Algebra.Construct.Pointwise`:
  ```agda
  isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# →
             IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
  
  nearSemiring : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ)

  ...etc...

[jamesmckinna]

... Yup! It's boring but exactly what's required.

[bsaul]

... Yup! It's boring but exactly what's required.

Cool. Added.

[jamesmckinna]

This will probably work, but let's see how it comes out in the wash after #2557 !