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

CC BY-SA 4.0
2020-11-30T16:18:23.010Z
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.
Astra Kolomatskaia
CC BY-SA 4.0
2020-12-01T08:12:14.223Z
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
CC BY-SA 4.0
2020-11-30T08:02:23.263Z
2020-11-30T08:08:01.467Z
2020-11-30T08:08:01.467Z
Andrej Bauer
<p>Addressing the question in the title: <span class="math-container">$\mathsf{\lambda n\,m.\,refl}$</span> is not a proof of commutativity <em>by definition</em> because addition is not a constant function by definition. Of course, the commutativity proof can be shown to be propositionally equal (by a &quot;dependent&quot; equality, or path-over-path) to the <span class="math-container">$\mathsf{refl}$</span>-returning one, by Andrej's answer. I focus on the definitional case here.</p>
<p>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.</p>
<p>If we have any <span class="math-container">$\mathsf{f : A \to A \to B}$</span>, then we can prove <span class="math-container">$\mathsf{f\,x\,y = f\,y\,x}$</span> by <span class="math-container">$\mathsf{refl}$</span> only if <span class="math-container">$\mathsf{f\,x\,y \equiv f\,y\,x}$</span>. By <span class="math-container">$\eta$</span>-expansion, <span class="math-container">$\mathsf{f}$</span> must be of the form <span class="math-container">$\mathsf{\lambda x\,y.\,t}$</span>, and the previous definitional equation becomes <span class="math-container">$\mathsf{t \equiv t[x \mapsto y, y \mapsto x]}$</span>.</p>
<p>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 <span class="math-container">$\mathsf{f}$</span> function must be of the form <span class="math-container">$\mathsf{\lambda \_\,\_.\,t}$</span>. As addition is not constant by definition, we cannot prove it commutative by <span class="math-container">$\mathsf{refl}$</span>.</p>

CC BY-SA 4.0
2020-11-30T23:45:28.670Z
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.
Astra Kolomatskaia
CC BY-SA 4.0
2020-11-30T23:47:42.107Z
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.
Astra Kolomatskaia
CC BY-SA 4.0
2020-11-30T10:47:08.447Z
2020-11-30T10:52:08.833Z
2020-11-30T10:52:08.833Z
András Kovács
<p>I've been curious about the '<em>geometric situation</em>' that one has when considering the type
<span class="math-container">$\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$</span>.
Here, addition is defined in the usual inductive way.</p>
<p>This proposition has an informative proof, which I will denote by <span class="math-container">$\textrm{plus-comm}$</span>. One interesting property that I've observed of this proof is that it computes to reflexivity on any specific <span class="math-container">$\textrm{Nat}$</span> values. I conjecture that this should be true of all terms of this type in my system.</p>
<p>That is, if <span class="math-container">$a$</span> and <span class="math-container">$b$</span> are <span class="math-container">$\textrm{Nat}$</span> <strong>values</strong>, then <span class="math-container">$(\textrm{plus-comm}\ a\ b) \equiv \textrm{refl}\ (\textrm{plus}\ a\ b)$</span>. For instance, this says that answering the question '<em>Why is 2+3 = 3+2?</em>' with '<em>Because the commutative law of addition holds</em>' reduces to '<em>Because both equal 5</em>'. (<em>In reference to a passage by Morris Klein. :P</em>)</p>
<p>We have a term
<span class="math-container">$$\lambda n, m. \textrm{refl}\ (\textrm{plus}\ n\ m) : \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m).$$</span></p>
<p>If we could show that the type <span class="math-container">$ \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m)$</span> equaled the type <span class="math-container">$\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$</span>, then this term yields* a valid proof of commutativity, which is something that I proximally find highly intuitively unappealing.</p>
<p>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.</p>
<p>* 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.</p>
<p>What is going on in this situation?</p>
<p><strong>TL;DR</strong>: We have that:
<span class="math-container">$$n, m:\textrm{Nat} \vdash (\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m).$$</span>
Why does it not follow that:
<span class="math-container">$$\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)?$$</span></p>

CC BY-SA 4.0
2020-11-30T02:32:22.743Z
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
CC BY-SA 4.0
2020-11-30T02:44:11.087Z
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.)
Astra Kolomatskaia
<type-theory><proof-theory><proof-assistants><homotopy-type-theory>
Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?
Astra Kolomatskaia
# Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?

(Asked by: username_0 on 2020-11-30)

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

**Tags:** type-theory, proof-theory, proof-assistants, homotopy-type-theory

> **Comments:**
> **username_1**: 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?  
> **username_0**: 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.)  

---

## 2 answers

### Answer by username_2 on 2020-11-30. Score: 5 | Accepted answer

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

> **Comments:**
> **username_0**: 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.  
> **username_2**: 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$.  

---

### Answer by username_3 on 2020-11-30. Score: 3

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

> **Comments:**
> **username_0**: 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.  
> **username_0**: 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.  

---

