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

• Of course, your conjecture is true: any proof of a concrete (closed) equality in MLTT reduces to refl. Of course this is not true with univalence. As a side note: are all the equalities in your question propositional equalities? What kind of extensionality are you assuming? – cody Nov 30 '20 at 2:32
• I am using $\equiv$ for all judgmental equalities. All others are propositional. Extentionality gives me an equivalence of types between proofs of point-wise (propositional) equality and proofs of function equality. (I know that judgmental exensionality follows from $\eta$-reduction on lambdas.) – Taras Kolomatski Nov 30 '20 at 2:44

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

• Thank you for the answer! There shouldn't be any homotoic information contained in the equivalence between these two types, but in order to define the equivalence, I would need: terms of each type to construct constant maps, and contractions of these types to the chosen points. In that case, the information that goes into the equality is sufficient that the transport operation can do something highly non-trivial like identify the two chosen terms. I'll keep this example in mind as a further study HoTT. – Taras Kolomatski Nov 30 '20 at 16:18
• The way I described the proof, the resulting transport operation from $A$ to $B$ is rather boring, as it is the constant map which ignores input and just produces one specific element of $B$. – Andrej Bauer Dec 1 '20 at 8:12

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

• Thanks for the answer! This is clear and a great argument. I suppose the one thing that I'm still unclear of is: The two types that I mentioned are not judgmentally equal, and in MLTT, any proof of equality in a closed context reduces to reflexivity. Thus, without extensionality and univalence, there should be no proof of the type' being equal. At the same time, there is something that intuitively suggests that this should be possible, if I think of equality elimination as 'replacing equals with equals'. The fact that the first equality depends on the context somehow plays a role. – Taras Kolomatski Nov 30 '20 at 23:45
• Is there an argument that I can't prove equality of my two types in a MLTT that does not recourse to saying that such a proof must reduce to reflexivity? Clearing this up would be very useful to my intuitions. – Taras Kolomatski Nov 30 '20 at 23:47