Pure equality vs defined definitional equality

[jaycech3n]

The theory thus far has been written to use the built-in Pure equality as the definitional equality, the idea initially being to take advantage of as much built-in functionality as possible.

However this creates may create differences between the implementation versus the formal type theory as presented in the book, e.g. the Martin-Löf type theory HoTT is based on does not have alpha-conversion, while the Pure equality does. [Edit: The situation is a little unclear. While the informal presentation in the HoTT book does mention alpha-conversion, the formalities in Appendix A2 do not really, and it's unclear how to use the existing judgment forms to express a change of bound variables.]

It would probably might be better to define a separate definitional equality on the object level for maximum compatibility with the theory in the book, though one would need to double check the theory.

[jaycech3n]

This is more of a question of how much we want to be able to do metatheory of HoTT inside Isabelle/HoTT. At some point this might be interesting to take a look at, but could end up being quite a bit of work.