[Agda] Fwd: Converting All2 to All

[Dr. ERDI Gergo]

On Sat, 6 Jan 2018, Matthew Daggitt wrote:

> Hi Gergo, So the first thing to say is that due to an oversight, the functionality of
> `All₂` in `Data.Vec.All` is actually a duplicate of the existing datatype
> `Relation.Binary.Vec.Pointwise`. In the upcoming release of the library at the end of
> January, we're deprecating `All₂` and moving `Relation.Binary.Vec.Pointwise` to
> `Data.Vec.Relation.InductivePointwise` and `Data.Vec.Relation.ExtensionalPointwise`.
> Feel free to have a look at the CHANGELOG in standard library repository for a more
> detailed explanation.

Thanks, that is a very useful heads-up. I've now migrated my code to 
D.V.R.InductivePointwise in anticipation of this change.

> That's not to say your proofs wouldn't be a welcome contribution to the library! The
> natural place for it in v0.15 will be in the new module
> `Data.Vec.Relation.InductivePointwise`. I would probably name them something
> like `pointwiseˡ⇒all` and `pointwiseʳ⇒all`, and possibly add their counterparts
> `all⇒pointwiseˡ` and `all⇒pointwiseʳ` as well. If you'd like to add them, feel free
> to submit a pull request to the library and they can be added to the upcoming release.

One snag, though, is that the current upgrade path of the stdlib requires 
D.V.All to import D.V.R.InductivePointwise, so I can't add these proofs to 
D.V.R.InductivePointwise without causing a circular import... the only 
place to add them currently is D.V.All. Would it still make sense for me 
to add them to D.V.All?