Remove mentions of the Id type

[plt-amy]

With the addition of indexed inductive types to Cubical Agda, having the built-in cubical identity type is redundant, since it has exactly the same computational behaviour as the indexed equality. However, cubical identity has its own support code for pattern matching, the Kan operations, and its magic type checking rule, which is now for no benefit. This PR removes the mentions of it from the library so I can remove it from Agda.

[maxsnew]

Is there somewhere I can read about this change? I just started using Cubical.Foundations.Id in a development so I don't understand how I am supposed to update my code

[JonasHoefer]

@maxsnew The inductively defined equality type in Cubical.Data.Equality has the same computational behavior as the one in Cubical.Foundations.Id and mostly the same interface. Furthermore, #1011 extends the module Cubical.Data.Equality slightly.

[mortberg]

I think this seems reasonable. What does @ecavallo think ? If you're happy feel free to merge

[ecavallo]

OK by me

[felixwellen]

Did you notice the conflicts?
Some large part of the issue addressed here was resolved in a different way in #1011

[felixwellen]

Something that was done here, but not in #1011 is deletion of things like Cubical.Core.Id, which I guess, would be good.

[mortberg]

Oops, I missed that.. Can @plt-amy update the PR to fix the conflicts and then we can merge?

[plt-amy]

Sure, I'll have a look later today 🙂

[mortberg]

Looks good to me! Is this ready to be merged?

[felixwellen]

Looks good (and ready) to me