This is accomplished by using the eliminator (or "recursor") of the natural numbers, known as "R".
The argument "PZ : P 0" becomes the base case "0+1 = 1+0", which is the term "refl nat 1".
Essentially, this says that when "x+1 = 1+x" has "x" replaced with a canonical value, the expression will be the same as "refl nat (x+1)".
For "extensional" versions, any identity type can be converted into a judgemental equality.
A computational version is known as "Axiom K" due to Thomas Streicher.