# Elimination rule for the equality type aka J axiom

I'm implementing a interpreter for lambda calculus, and now I want to add the equality type. The introduction rule for it is easy, but the elimination rule is rather obscure for me. I found this stackoverflow thread, but it explains the J axiom only in one sentence. How can it be understood intuitively?

A complete understanding of what J was actually saying and why has only come fairly recently. This blog post discusses it. While thinking in terms of homotopy and continuous functions provides a lot of intuition and connects to a very rich area of mathematics, I'm going to try to keep the discussion below at the logical level.

Let's say you axiomatized equality types directly (these are groupoid operations and laws): $$\frac{\Gamma\vdash x:A}{\Gamma\vdash \mathbf{refl}_x : x=_A x} \qquad \frac{\Gamma, x:A, y:A\vdash p : x=_A y}{\Gamma, x:A, y:A\vdash p^{-1} : y =_A x} \qquad \frac{\Gamma, x:A, y:A\vdash p : x=_A y \quad \Gamma,y:A, z:A\vdash q : y=_A z}{\Gamma, x:A, y:A, z:A\vdash p\cdot q : x =_A z}$$ $$(p^{-1})^{-1} \equiv p \qquad p\cdot p^{-1} \equiv \mathbf{refl} \qquad (p\cdot q)^{-1} \equiv q^{-1}\cdot p^{-1} \\ \mathbf{refl} \cdot p \equiv p \equiv p \cdot \mathbf{refl} \qquad (p \cdot q) \cdot r \equiv p \cdot (q \cdot r)$$ We have substitution which is functorial. $$\frac{\Gamma, z : A\vdash F(z) : \mathbb{U}\qquad\Gamma,x:A,y:A\vdash p : x=_A y}{\Gamma, x:A,y:A\vdash \text{subst}(F,p) : F(x) \to F(y)}$$ $$\text{subst}(F,\mathbf{refl}) = \text{id} \quad \text{subst}(F,p\cdot q) = \text{subst}(F,q)\circ\text{subst}(F,p)\\\text{subst}(\lambda x.c=_A x,p)(q) = q\cdot p$$ Finally, we would have congruence rules for everything, saying everything respects this equality. Here is one of the most important congruences. $$\frac{\Gamma, x:A, y:A\vdash p : x=_Ay \quad \Gamma,z:A\vdash B(z) : \mathbb{U}}{\Gamma, x:A, y:A, b : B(x)\vdash \text{lift}_B(b,p) : \langle x,b\rangle =_{\Sigma x:A.B(x)}\langle y,\text{subst}(B,p)(b)\rangle}$$

Now let's consider a special case of substitution. $$\frac{\Gamma\vdash c:A \quad \Gamma,t:\Sigma x\!:\!A.c=_Ax\vdash C(t):\mathbb{U} \quad \Gamma\vdash b : C(\langle c,\mathbf{refl}_c\rangle)}{\Gamma,y:A,p:c=_Ay\vdash\text{subst}(C,\text{lift}_{\lambda z.c = z}(\mathbf{refl}_c,p))(b) : C(\langle y,p\rangle)}$$

This is J. We can use currying to get the nicer looking form:

$$\frac{\Gamma\vdash c:A \quad \Gamma, y:A, p : c=_A y \vdash C(y,p): \mathbb{U} \quad \Gamma\vdash b : C(c,\mathbf{refl}_c)}{\Gamma, y:A,p : c=_A y\vdash J_{A,c}(C,b,y , p) : C(y,p)}$$

Of course, if we start with J we can rederive all the other structure I defined.

Now if we have $p : x =_A y$ and $q : y =_A y'$ then $\text{lift}_{\lambda z.x=z}(p, q) : \langle y,p\rangle = \langle y',p\cdot q\rangle$. So if we have $\langle y', p' \rangle$, there's no way to get to it from $\langle y,p\rangle$ via a pre-selected $q$ in general unless $p \cdot q = p'$. (From the homotopy perspective, $p \cdot q = p'$ says we can fill in the triangle with edges $p$, $q$, and $p'$.) To make it more blunt, set $p = \mathbf{refl}_x$ (and $y=x$) and we get $q = p'$ being the required equality which is not true in general (because a value of type $x =_A y'$ can represent an arbitrary equivalence and there's nothing saying two equivalences have to be the same, or, equivalently, because we know groupoids can be non-trivial). The point of this is to demonstrate that things can be equal in more than one way, i.e. one value of $y = y'$ is not as good as another in general.

A key thing to understand is that J says the type $\Sigma y\!:\!A.x=_Ay$ is inductively defined, and says little about the type $x=_Ay$ for fixed $x$ and $y$. One way to see this, and why J is the way it is, is to look at what congruence at equality types with matching endpoints looks like. We have the following rule (ignoring the proof term, it's expressible with $\text{subst}$ or J): $$\frac{\Gamma, x:A\vdash p : x=_Ax}{\Gamma, x:A, q : x =_A x\vdash \_ : q =_{x=_Ax} p \cdot q \cdot p^{-1}}$$ With $\text{lift}_{\lambda z.x=z}$ we have the option of doing $\text{lift}_{\lambda z.x=z}(p, p^{-1}\cdot p') : \langle y,p\rangle = \langle y',p'\rangle$ so every point was equivalent to every other point (though not necessarily trivially). With both endpoints matched, we don't have the flexibility of choosing the equalities to first cancel out the input equality and then performing an arbitrary equality.

While J carefully respects the non-trivial groupoid structure of equality types, in typical dependently typed languages there's no way to actually define a non-trivial element of an equality type. At this point you hit a fork in the road. One route is to add Axiom K which says that the groupoid is actually trivial which makes many proofs much simpler. The other route is to add axioms that allow you to articulate the non-trivial groupoid structure. The most dramatic instance of this is the Univalence Axiom which leads to Homotopy Type Theory.

• For the next person who sees it: this whole answer only makes sense after you understand homotopy type theory. – 盛安安 Oct 10 '16 at 18:43
• Are there interesting but less dramatic ways of expressing non-trivial equalities than Univalence Axiom ? – Łukasz Lew Jul 6 '18 at 23:35
• @ŁukaszLew You could take results implied by univalence without taking the whole thing. Univalence gives you an $(\infty,1)$-groupoid, but you could assert only a limited number of homotopy levels (indeed, this is effectively what Axiom K does). You could also assert the existence of particular types with non-trivial identity types, e.g. $\mathbb S^1$, or assert that a pre-existing type has some non-trivial elements in its identity type. – Derek Elkins left SE Jul 7 '18 at 3:22
• @ŁukaszLew It doesn't give everything I mentioned. The existence of $\mathbb S^1$ goes beyond univalence. It and its structure either need to be asserted explicitly, or higher inductive types are required. Univalence, in some sense, only talks about the identity types for the universe(s). – Derek Elkins left SE Jul 7 '18 at 19:20
• @ŁukaszLew As a minor correction $\mathbb S^1$ is representable (albeit, I believe in a slightly weaker way than a higher inductive type would give). Nevertheless, I don't believe it is known whether all higher spheres are or not. The point is higher inductive types are a separate scheme of axioms neither dependent on nor derivable from univalence, though coming from the same intuitions and certainly interacting. – Derek Elkins left SE Jul 22 '18 at 3:47