Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?

Question

I've been curious about the 'geometric situation' that one has when considering the type $\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$. Here, addition is defined in the usual inductive way.

This proposition has an informative proof, which I will denote by $\textrm{plus-comm}$. One interesting property that I've observed of this proof is that it computes to reflexivity on any specific $\textrm{Nat}$ values. I conjecture that this should be true of all terms of this type in my system.

That is, if $a$ and $b$ are $\textrm{Nat}$ values, then $(\textrm{plus-comm}\ a\ b) \equiv \textrm{refl}\ (\textrm{plus}\ a\ b)$. For instance, this says that answering the question 'Why is 2+3 = 3+2?' with 'Because the commutative law of addition holds' reduces to 'Because both equal 5'. (In reference to a passage by Morris Klein. :P)

We have a term $$\lambda n, m. \textrm{refl}\ (\textrm{plus}\ n\ m) : \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m).$$

If we could show that the type $ \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m)$ equaled the type $\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$, then this term yields* a valid proof of commutativity, which is something that I proximally find highly intuitively unappealing.

Now, I can't seem to prove the equality stated above from commutativity, and I imagine that there is a good reason for why this is impossible.

* I am assuming extensionality and univalence. Thus, an equality of said types would yield an equivalence by which I could map the reflexivity term. However, the types in question shouldn't have any non-trivial higher groupoid structure, so I don't imagine that HoTT operations would perform any non-trivial computations (such as identifying these two proofs) in this setting. If the resolution of this question involves HoTT ideas, then I would be very intrigued.

What is going on in this situation?

TL;DR: We have that: $$n, m:\textrm{Nat} \vdash (\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m).$$ Why does it not follow that: $$\vdash \left(\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m)\right) = \left(\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)\right)?$$

Answer 1

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$.

Answer 2

Addressing the question in the title: $\mathsf{\lambda n\,m.\,refl}$ is not a proof of commutativity by definition because addition is not a constant function by definition. Of course, the commutativity proof can be shown to be propositionally equal (by a "dependent" equality, or path-over-path) to the $\mathsf{refl}$-returning one, by Andrej's answer. I focus on the definitional case here.

Assume that we are working in a normalizing intensional type theory. For our purposes, we can view HoTT as normalizing as well, we can just work under the assumption of univalence in the typing context.

If we have any $\mathsf{f : A \to A \to B}$, then we can prove $\mathsf{f\,x\,y = f\,y\,x}$ by $\mathsf{refl}$ only if $\mathsf{f\,x\,y \equiv f\,y\,x}$. By $\eta$-expansion, $\mathsf{f}$ must be of the form $\mathsf{\lambda x\,y.\,t}$, and the previous definitional equation becomes $\mathsf{t \equiv t[x \mapsto y, y \mapsto x]}$.

It follows from somewhat tedious induction on normal forms that if a term is unchanged under renaming a bound variable to a different one, then the variable cannot occur in the normal form of the term. Hence, the original $\mathsf{f}$ function must be of the form $\mathsf{\lambda \_\,\_.\,t}$. As addition is not constant by definition, we cannot prove it commutative by $\mathsf{refl}$.