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.

StackExchange Computer Science Q#53081, answer score: 8