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)?$$