Context: type theory.
My understanding of:
- WN: every term can rewrite to NF.
- Canonicity: every term rewrites into canonical form.
Then it leads to an intuition where if canonicity holds, then we get NF = canonical form and therefore WN holds. However, I don't see people state this often, like this question talks about canonicity but never mentions NF or normalization. On nLab, canonical form is said to be normal form, which justifies my "NF = canonical form" guess but it doesn't say WN therefore holds. Therefore I'm doubting my intuition.
So, I wonder if it's right (is there a proof?), or if it's wrong (is there a counterexample?).