All axioms break canonicity?

[nielsvoss]

Describe the error

In 3.2.2. Propositions:

It does however block computation when using #reduce to reduce proofs directly (which is not recommended), meaning that canonicity, the property that all closed terms of type Nat normalize to numerals, fails to hold when this (or any) axiom is used:

Why is it incorrect and/or confusing?

I'm not sure what you mean by "or any". Do all axioms break canonicity, even if they have nothing to do with Nat or propositions? Maybe it's correct, I was just a little confused. Also, for people new to type theory, it might not be clear that axiom specifically refers to terms defined with the axiom command, rather than all the inference rules that built in to the type theory, and then it would be really confusing to read that all axioms break canonicity (although maybe this isn't a problem for the target audience).