agda
Add properties of `Data.Refinement` and refactor module structure
NB.
- could be folded into
Data.Refinementdirectly? - Fairbairn threshold? is this injectivity proof not immediate?
Yup, I this is definitely useful! Also I think
Propertiesis 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/.Propertiesdivision? (also could be handled downstream)
Yes please: if it grows enough, let's split it up according to the hierarchy!
OK, I've added a proof of (inheritance of) DecidableEquality, and refactored module structure in terms of Base/Properties.
I'll stop there.
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?
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.
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.
