Add properties of Data.Refinement and refactor module structure

[jamesmckinna]

NB.

• could be folded into Data.Refinement directly?
• Fairbairn threshold? is this injectivity proof not immediate?

[MatthewDaggitt]

Yup, I this is definitely useful! Also I think Properties is definitely the right place for it, even though it seems like overkill at the moment. I'm sure more stuff will be added to it!

[jamesmckinna]

Yup, I this is definitely useful! Also I think Properties is definitely the right place for it, even though it seems like overkill at the moment. I'm sure more stuff will be added to it!

Two things:

• I do have some additional properties (concerning iterated refinement, and decidability) which occurred to me during the writing of this (downstream PR?)
• Should we followup with a refactoring into an orthodox .Base/.Properties division? (also could be handled downstream)

[gallais]

Yes please: if it grows enough, let's split it up according to the hierarchy!

[jamesmckinna]

OK, I've added a proof of (inheritance of) DecidableEquality, and refactored module structure in terms of Base/Properties.

I'll stop there.

[jamesmckinna]

Does @fredrikNordvallForsberg 's resolution of #2495 mean that we could simplify the implementation of Data.Refinement to simply make the proof field take the . modality?

record Refinement {a p} (A : Set a) (P : A → Set p) : Set (a ⊔ p) where
  constructor _,_
  field value : A
        .proof : P value
infixr 4 _,_
open Refinement public

module _ {P : A → Set p} {Q : B → Set q} where

  map : (f : A → B) → ∀[ P ⇒ f ⊢ Q ] →
        [ a ∈ A ∣ P a ] → [ b ∈ B ∣ Q b ]
  map f prf (a , p) = f a , prf p

etc.

Not for this PR, but a potential simplifying, even if breaking, refactoring/deprecation downstream?

[gallais]

You don't get irrelevant projections so IME it's nicer to package up things affected by the irrelevant
modality so that you can project them out and pass them around to combinators.

[JacquesCarette]

The old category library used to use irrelevance a lot and then broke in ways we couldn't fix at some point in Agda's evolution. So I'd be quite concerned that we'd run up against bugs "just too late" if we start using it too much in the library.

Irrelevant projections (and the lack thereof) are a big deal. Conor and I more recently tried to use irrelevance quite aggressively to force Agda to ensure we stay honest (we're doing quotients "by hand"), and gave up. Now we stay honest by sheer force of will.

[jamesmckinna]

Ready to merge now?

[jamesmckinna]

This is clearly a pattern, which currently is reified only under Relation.Decidable.Nullary.Decidable.via-injection, but it seems excessive to create an Injection bundle solely for the sake of applying the lemma, so suggest some downstream refactoring to make this a property of Injective (bare) functions?