# Homotopy type theory: why are $0:\mathbb N$ and $\mathrm{succ}(0):\mathbb N$ not judgementally equal?

Section 2.13 in The HoTT Book uses "the encode-decode method to characterize the path space of the natural numbers" by defining a type family:

$$\mathrm{code} : \mathbb N \to \mathbb N \to \cal U$$

with

$$\begin{array}{rcl} \mathrm{code}(0,0) & :\equiv & \mathbf 1\newline \mathrm{code}(\mathrm{succ} (m),0) & :\equiv & \mathbf 0\newline \dots & :\equiv & \dots\newline \dots & :\equiv & \dots \end{array}$$

To my understanding, $$\mathrm{code}$$ is only well-defined, if (in particular) $$0:\mathbb N$$ and $$\mathrm{succ}(0):\mathbb N$$ are not judgementally equal. How can we be sure that this is the case?

Daniel's answer is correct that the judgmental distinctness of $$0$$ and $$\mathsf{succ}(m)$$ is not what justifies a definition by pattern-matching. However, it is still a meaningful question of how to prove that $$0$$ and $$\mathsf{succ}(m)$$ are not judgmentally equal. (Stretching terminology a bit, Daniel answered your X and I'm going to answer your Y.)

Note that this is a metatheoretic question, in contrast to the internal proof that $$0\neq \mathsf{succ}(m)$$. Thus, even though judgmental equality implies typal equality, the answer to that question does not answer this one.

It's also worth noting that this is not a trivial question, even though $$0$$ and $$\mathsf{succ}$$ are distinct constructors. From an "algebraic" perspective on type theory, judgmental equality is just the smallest congruence generated by certain rules. Thus, two terms that don't "look" like they could possibly be equal might turn out to be equal by passing through some chain of forwards and backwards equalities to other terms.

For the same reason, it is a "global" question about the type theory, not one that can be answered by referring only to $$\mathbb{N}$$. For instance, in a higher inductive type such as the interval $$\mathsf{I}$$, with constructors $$\mathsf{zero},\mathsf{one} : \mathsf{I}$$ and $$\mathsf{seg}:\mathsf{zero}=\mathsf{one}$$, there is no "local" reason for $$\mathsf{zero}$$ and $$\mathsf{one}$$ to be judgmentally equal; but if the type theory also includes the equality reflection rule, then $$\mathsf{seg}$$ implies that $$\mathsf{zero}\equiv\mathsf{one}$$.

One answer to this question involves giving an algorithm for checking whether two terms are judgmentally equal. Probably the simplest such algorithm involves giving a "rewriting system" under which every term can be reduced to a "normal form", and then two terms are judgmentally equal if they reduce to the same normal form (up to $$\alpha$$-equivalence). Roughly speaking, this rewriting system consists of what the HoTT Book calls "computation rules". One then has to prove that this rewriting system is terminating, and that the relation of "reducing to the same normal form" is a congruence; thus it coincides with judgmental equality. Then one can simply observe that $$0$$ and $$\mathsf{succ}(m)$$ are (when $$m$$ is a variable) distinct normal forms.

In practice, nowadays more complicated algorithms are used. Among other reasons, this is in order to also include what the HoTT Book calls "uniqueness rules". These algorithms often go by names like "normalization by evaluation". The crucial idea is that there are two "phases" of the algorithm, one which applies the computational rewrites, and another which applies the uniqueness rules in the expansionary direction ($$f \mapsto (\lambda x. f(x))$$ or $$u \mapsto (\pi_1(u),\pi_2(u))$$) by inspecting their types. But the basic idea is the same: after proving that the algorithm is terminating and complete, we can run the algorithm on two terms to verify that they are unequal (or equal).

With that said, I don't know whether anyone has actually done this for Book HoTT. It's known for MLTT, on which Book HoTT is based, but Book HoTT adds not just axioms (which don't disrupt such an algorithm) to MLTT but new judgmental equalities (the computation rules for point-constructors of HITs), which then have to be incorporated in the algorithm. So (even laying aside the point that "Book HoTT" is not precisely specified because it is open-ended with respect to what HITs are definable) there may technically be an open question here. However, I think no type theorist who's familiar with such proofs would have much doubt that standard techniques ought to apply to Book HoTT (and it's possible that someone has already done it).

Edit: Simon has pointed out in the comments what I should clearly have realized myself, namely that another way to deduce that two terms are not judgmentally equal is to give a model in which they are interpreted by distinct things. Thus, for instance, the set-theoretic model proves this for MLTT, and the simplicial set model proves it for Book HoTT (modulo details in the construction of that model that aren't yet in the literature, such as showing that the univalent universes are closed under a sufficiently large class of higher inductive types).

• I agree that there is no "syntactic consitency proof" like what you are talking about, but I would argue that the existence of the simplicial model shows that Hott doesn't prove $0 \equiv S 0$. Maybe it is worth adding that if "Model of HoTT" is taken to mean "contextual category with all the structure needed to interpret all the type constructor present in Book HoTT" (which I think is the commonly accepted notion of models) then there is indeed a "trivial model" of HoTT in which $0 \equiv S0$. Oct 12, 2022 at 15:49
• Of course, the previous comment is potentially conditional on the initiality conjecture depending on how things are defined.... Oct 12, 2022 at 15:53
• Yes, you're right! Oct 13, 2022 at 4:25
• There are still gaps other than the initiality conjecture/theorem, though: in particular the closure of universes under HITs doesn't yet appear in the literature. Oct 13, 2022 at 4:29
• Thanks, Mike and Simon, that clarified a lot for me. Although the metatheoretic machinery has not been completely laid out in Book HoTT, I assume that there is at least an implicit assumption on how things were to work out if explained in all detail. My interpretation according to your answers: (1) Book HoTT "intents" distinct constructors to construct judgementally different elements. (2) For a given constructor function f:A->A, the terms f^n (a) and f^m (a) are not judgementally equal for n<>m -- unless maybe there is a definition of a rule on how f can be eliminated in such expressions.
– Bodo
Oct 17, 2022 at 12:19

It's a bit confused to view $$\mathsf{code}$$ as well-defined because 0 and its successor are not definitionally equal. Rather, it's well-defined because of the induction principle associated with the natural number type; the pattern-matching notation is a shorthand for invoking the induction principle. See Section 1.9 of the HoTT book for a discussion of this induction principle.

If we lacked this induction principle, even if $$0$$ and $$\mathsf{succ}(0)$$ were not definitionally equal we would not be able to define $$\mathsf{code}$$ in this way.

• Thanks, Daniel, for pointing out the confusion inherent in my question. Let me try to clarify what I actually intented to state: If we do not know whether 0 and succ(0) (and more general: 0 and succ(m)) are judgementally equal, then we do not know whether the given definition of code leads to problems, e.g. to a contradiction. Does this make (more) sense to you?
– Bodo
Oct 17, 2022 at 11:39
• So if we have (1) the induction principle for natural numbers and (2) a judgmental equality between $0$ and $1$, then we can construct an element $x$ of the empty type $\mathsf{False}$. So those two things together produce an inconsistency. But this argument is actually how we deduce that $0$ and $1$ are not definitionally equal. Oct 17, 2022 at 17:04
• The argument (as mike outlined above) goes like this. Suppose $0$ and $1$ were definitional equal, then HoTT would have a proof of false. Then any model of HoTT would have an element in whatever we used to interpret $\mathsf{False}$, but there is a model of HoTT (in simplicial sets) which interprets the empty type in such a way that it has no elements. Therefore, $0$ is not definitionally equal to $1$ in HoTT. Oct 17, 2022 at 17:05
• I don't think you need to bring in the empty type. Just observe that in the model in simplicial sets, 0 and 1 are distinct; thus, they cannot be definitionally equal in the theory. Oct 18, 2022 at 2:37
• Oh, good point! @MikeShulman Oct 19, 2022 at 9:26

As Daniel explained, the induction principle associated with $$\mathbb{N}$$ allows you, by definition, to define $$code$$ in this way, even if $$0$$ and $$succ(0)$$ were judgmentally equal. In such a situation, $$code$$ would still be well defined, but this would result in an inconsistent theory, where 0 would be judgementally equal to 1, and therefore inhabited.

A metatheoretic justification that HoTT is consistent is therefore a justification that $$0$$ and $$succ(0)$$ are not judgmentally equal.

• Thanks, L., for your answer. I think that I perfectly understood the first paragraph of your answer. However, I am not sure that I completely grasped the content of the second paragraph. Could you please elaborate on what you mean by "is therefore a justification that"?
– Bodo
Oct 17, 2022 at 11:46