Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?
But it does follow. The types
$$A = \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m)$$
and
$$B = \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$$
are both contractible. Indeed, they are both inhabited and because $\mathrm{Nat}$ is a set, its identity type is a proposition, hence so are $A$ and $B$, as they are products of propoitions. An inhabited proposition is contractible.
Any two contractible types are equivalent, $A \simeq B$, thus by univalence also propositionally equal (as elements of a universe), $A = B$. However, $A$ and $B$ are not judgementally equal.
Consequently, the term $t = \lambda n, m \,.\, \mathrm{refl} (\mathrm{plus}\,n\,m)$ has type $A$ but it does not have type $B$. We can however transport $t$ along an equivalence $e : A \to B$ to obtain a term $e\,t : B$.