Reed Mullanix
Reed Mullanix
So I've done some experimentation with this, and I think we should go a step further. This does clean up a _lot_ of stuff, but there are still places where...
The reason I didn't use that is that it doesn't play as nice with multiline proofs. For instance, it's very easy to just do ```agda fun-eq λ x → let...
The two definitions are indeed equivalent. ```agda import Relation.Binary.Reasoning.Setoid as SR module _ {c ℓ} {A B : Setoid c ℓ} (f g : A ⟶ B) where module A...
IIRC it was somewhat unclear what the plans were in the stdlib for the new function hierarchy. Could be misremembering though!
I'd be more than happy to help out!
I like `Categories.Topos.Pretopos`, as it is nice and discoverable, and also serves as a nice folder structure for various riffs on pretopoi, IE: `Categories.Topos.Pretopos.Heyting`. On a related note, I've looked...
Huge 👍 from me! I would even go so far as adding a disclaimer at the top saying "this is probably not what you want", and try to direct people...
I have a preliminary implementation of sieves that might be useful for this. Will tidy it up and make a PR in the next few days.
I remember writing this a few months ago. It was before the middleware system came into place, but I'm sure adapting it wouldn't be too difficult.
Sadly, that code was commercial, so no :frowning_face:.