G. Allais

I think the people who were tired of typing `Relation.Binary.PropositionalEquality` are not going to like it. :D Pragmatically, is this issue actually an Agda feature request in disguise for 1....

You have pushed the change to [the divmod PR](https://github.com/agda/agda-stdlib/pull/1191/)

FYI we are using 2.5G of heap on the stdlib travis instance: https://github.com/agda/agda-stdlib/blob/master/.travis.yml#L67

I think the plan is to use `_

Is `_≉_` from a setoid? So it's more like a triple than a pair then.

Should `Data.Nat` export [`

Surely local flags cannot invalidate the ones set globally?

So this means that we cannot trust a `--safe` in the lib file. This is distressing.

Note that you can quickly write something equivalent using the `Relation.Unary` combinators: `∀[ P ⇒ f ⊢ P ]`.

@jamesmckinna We do have some of these things, following from our discussions :) http://agda.github.io/agda-stdlib/Relation.Unary.Closure.Base.html http://agda.github.io/agda-stdlib/Relation.Unary.Closure.Preorder.html http://agda.github.io/agda-stdlib/Relation.Unary.Closure.StrictPartialOrder.html