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.
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
createsmay 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 probablymight 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.