add subst0 to substitute erased equalities in non-erased types

[liesnikov]

No description provided.

[jespercockx]

The error message from failing CI:

Cannot make function subst0 transparent. A transparent function must have exactly one non-erased argument and return it unchanged.

I guess that you need to make the p argument erased (or implicit, but that isn't as nice).

[flupe]

• Could you move it to Haskell.Law.Equality?
• Can you also erase the a argument --- in practice I've found it necessary when using datatypes and records defined as @0.

[liesnikov]

We discussed placement with @jespercockx and the reason to put it in Prelude was that subst0 seems closer to coerce than anything in Law.Equality. I don't mind either way but would be good not to move it back the day after 🙃 .

Pushed the update on the erasure of a. Also marked it as implicit, not sure if there's a general policy on this?

[flupe]

The difference being coerce is a function that shows up in Haskell code as a function from Haskell base. subst0 isn't related to anything on the Haskell side, it's a purely Agda-side construct about equality, just like things in Haskell.Law.Equality.

For that matter, I don't think coerce should be named coerce or be in Haskell.Prelude, if our goal is to replicate the Haskell prelude structure.

Even if you end up not putting subst0 in Law.Equality, we should stop putting things in Prelude by default.

[liesnikov]

I really really don't mind, if it gets merged faster with it being in Law.Equality I'm happy to put it there.
Pushed the move just now.