Ytukyg

In homotopy type theory, there are two notions of equality. There's the internal propositional equality, $=$, and the stronger, more-meta judgemental equality, $equiv$. My question is, is $x equiv y$ the same as all of the following holding:

$$
p_1 : x=y,quad p_2 : p_1=text{refl}, quad p_3 : p_2 = text{refl}, quad ldots
$$

? My intuition says yes, but this stuff gets so self-referential that I can hardly keep it straight. Here's my thinking: a type $A:mathscr{U}$ is a topological space in HoTT. So I'm visualizing it as the disjoint union of a bunch of path-connected spaces, where two points are in the same subspace iff they're propositionally equal. Judgemental equality, as the strongest possible equality, holds iff they're actually the same point. Reflection is the constant path, so then we ought to have $x equiv y$ iff $p_1 : x = y, quad p_1 equiv text{refl}$. If that's right, then you can use the same idea to turn $p_1 equiv text{refl}$ into $p_2 : p_1 = text{refl}, quad p_2 equiv text{refl}$, and just keep doing that ad-infinitum.

Is the above picture correct, or even coherent? If not, what's a better visual?

EDIT: It's been explained to me that what I said obviously can't be true as written; e.g., $text{base} equiv text{base}$ despite $text{loop} : text{base} = text{base}$ and $text{loop} notequiv text{refl}$. So to rephrase, is it true if you existentially quantify everything? That is, does $x equiv y$ hold iff there exists a $p_1, p_2, p_3, ldots$ (all of which are proofs that the next lower level is reflection)?

I think the answer to your question (existentially reformulated) is "yes", but not for the reason you probably think. In fact as soon as you have $p_1:x=y$ and $p_2:p_1={rm refl}$, it must be that $xequiv y$. The reason is that equality is "homogeneous": it only makes sense to talk about whether $x=y$ once you know that $x$ and $y$ have the same type (hence why we sometimes write $x=_A y$). So in particular, it only makes sense to talk about $p_2:p_1={rm refl}$ once you know that $p_1$ and ${rm refl}$ have the same type. But $p_1$ has type $x=y$ and ${rm refl}_x$ (say) has type $x=x$, while terms have unique types (modulo subtleties like subtyping and universe cumulativity) so it must be that the types $x=y$ and $x=x$ are (judgmentally) equal, $(x=y)equiv (x=x)$. Finally, type constructors are (judgmentally) injective, so for instance $(a=b) equiv (c=d)$ can only happen if $aequiv c$ and $bequiv d$; hence in this case we must have $yequiv x$.

The reason I say that this is probably not what you're thinking about is that it's basically syntactic trickery, due to the way that the syntax is usually formulated and the fairly finicky properties (like unique types and injectivity of type formers) that it usually has. Moreover, these properties are "admissible" rather than "derivable", which means that the above argument is not a proof inside HoTT (or more precisely a "derivation"), rather it is a meta-argument about derivability: whenever you can derive $p_1:x=y$ and $p_2:p_1={rm refl}$ it must also be the case that you can derive $xequiv y$.

Here's an example that I think may be more along the lines you have in mind which shows that the answer to the question you probably meant to ask is "no". Suppose $A$ is a contractible type, so that for any $x,y:A$ we have $x=y$. In fact, if $A$ is contractible then the type $x=y$ is also contractible. Thus, for $x,y:A$ we have some $p_1:x=y$, and for any $q_1:x=y$ we have $p_2:p_1=q_1$; and for any $q_2:p_1=q_1$ we have $p_3:p_2=q_2$; and so on. But this doesn't imply $xequiv y$. For instance, we could take $A = sum_{b:S^1} (b={rm base})$; then $A$ is contractible, but the two points $({rm base},{rm refl})$ and $({rm base},{rm loop})$ of $A$ are not judgmentally equal, since if they were then we would have ${rm refl} equiv {rm loop}$ which cannot be true. (Note that any proof of "judgmental inequality" must also be a meta-argument that "judgmental equality is not derivable", since the formal system of type theory does not allow derivations of judgmental inequality.)