If \(x\) and \(y\) are equal, we write \(x\)\(\;\equiv\;\)\(y\). What does that mean? It means \(x\) and \(y\) are just the same thing. And what does that mean? It means if a term involves \(x\), it can be changed to \(y\) .
The bewilderment arises, if we consider \(x\)\(\;\equiv\;\)\(5\), \(y\)\(\;\equiv\;\)\(3\). Then \(x\) and \(y\)\(\,+\,\)\(2\) are the same thing. But how can \(x\)\(\;\equiv\;\)\(y\)\(\,+\,\)\(2\) happen? The left side is the identifier for a constant, and the right side is the result of an operation involving an identifier for a constant and another constant.
If everything is phrased as something existing or something producing something else, then an identity is an object in a type too. If \(x\) and \(y\) are identical, we have a algorithm \(\varphi\) which verifies the fact. Object \(\varphi\) has type \(I\)\(\left[\vphantom{x ,\, y}\right.\)\(x\)\(,\,\)\(y\)\(\left.\vphantom{x ,\, y}\right]\), traditionally denoted \(x\)\(\;=\;\)\(y\). The identity \(I\) depends on a type \(A\), and it relates two objects of the same type as follows:
\(I\)\(\left[\vphantom{A :\, \wp ,\, a :\, A ,\, b :\, B}\right.\)\(A\)\(:\,\)\(\wp\)\(,\,\)\(a\)\(:\,\)\(A\)\(,\,\)\(b\)\(:\,\)\(B\)\(\left.\vphantom{A :\, \wp ,\, a :\, A ,\, b :\, B}\right]\)\(:\,\)\(\wp\)\(;\,\)
Every term is equal to itself, and every object in a type may be replaced with equal objects, namely:
\(\;\mathtt{given}\;\)\(x\)\(:\,\)\(A\)\(,\,\)\(\;\mathtt{has}\;\)\(\mathscr{R}\)\(\left[\vphantom{x}\right.\)\(x\)\(\left.\vphantom{x}\right]\)\(\;\equiv\;\)\(\psi\)\(:\,\)\(I\)\(\left[\vphantom{A ,\, x ,\, x}\right.\)\(A\)\(,\,\)\(x\)\(,\,\)\(x\)\(\left.\vphantom{A ,\, x ,\, x}\right]\)\(;\,\)
\(\;\mathtt{given}\;\)\(x\)\(,\,\)\(y\)\(:\,\)\(A\)\(\;\mathtt{and}\;\)\(C\)\(:\,\)\(A\)\(\:\Rightarrow\:\)\(\wp\)\(,\,\)\(\;\mathtt{has}\;\)\(\mathscr{L}\)\(\left[\vphantom{\varphi :\, I \left[A ,\, x ,\, y\right]}\right.\)\(\varphi\)\(:\,\)\(I\)\(\left[\vphantom{A ,\, x ,\, y}\right.\)\(A\)\(,\,\)\(x\)\(,\,\)\(y\)\(\left.\vphantom{A ,\, x ,\, y}\right]\)\(\left.\vphantom{\varphi :\, I \left[A ,\, x ,\, y\right]}\right]\)\(\;\equiv\;\)\(\psi\)\(:\,\)\(I\)\(\left[\vphantom{\wp ,\, C \left[x\right] ,\, C \left[y\right]}\right.\)\(\wp\)\(,\,\)\(C\)\(\left[\vphantom{x}\right.\)\(x\)\(\left.\vphantom{x}\right]\)\(,\,\)\(C\)\(\left[\vphantom{y}\right.\)\(y\)\(\left.\vphantom{y}\right]\)\(\left.\vphantom{\wp ,\, C \left[x\right] ,\, C \left[y\right]}\right]\)\(;\,\)
A moment’s thought reveals reflexivity, symmetry, and transitivity hold, and therefore the identity type can be viewed as an equivalence relation, agreeing the tradition notion.
When we stated the rules, we used the judgemental equality. However, we see immediately if \(x\)\(\;\equiv\;\)\(y\) then \(x\)\(\;=\;\)\(y\) . This is the reason that it is mostly harmless to confuse them. In presenting classical mathematics, we would use \(\;\equiv\;\) only in definitions, and use \(\;=\;\) elsewhere.
Actually, in formulating the rules, it was possible to altogether avoid \(\;\equiv\;\) nor introduce \(\;=\;\), in favor of the judgement sign \(\;\vdash\;\); though the rules would be harder to understand to most people. If so, the judgemental equality would be merely a syntactic sugar. Anyway for our purpose, whenever it is called, \(\;\equiv\;\) is considered as \(\;\equiv\;\), unless when it really can’t.
❧ August 12, 2021