Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition? 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)?$$
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$.