I'm interested in HoTT, especially its application to foundations of mathematics.
I believe strongly that Univalent Foundations is the very foundation of mathematics.
So,I have a question.
(Q) Univalent Foundations(or such variant systems of HoTT that provide a foundation of mathematics) and canonicity property are compatible?
Of course, the answer to the question depends on the definition of such systems.
Indeed the system in Appendix A.1 in the HoTT book has canonicity property,
while the system in Appendix A.3 doesn't.
But regardless of the definition of such systems, in order to provide a foundation of mathematics, they should have at least the following property.
For any computable function, there exist a term express that function in the system.
The above requirement may be irrelvant,but I want to require it here.
Then,in the above context,I want to ask (Q).
My own answer to the question is the following.
As far as I understand, any type system that has canonicity isn't Turing complete.
So,there is a computable function that can't be expressed in such system.
Therefore, by the above definition of such systems,
any formalization of HoTT as a foundation of mathematics(in the above sense) can't be compatible with canonicity.
Is it right?