In the following I write “$\dots$” for some formal necessary context declarations, but which don't help understanding the rules.
| ${\large\frac{\dots\ \vdash\ A\,:\,\mathrm{Type}}{x,y\,:\,A\ \vdash\ Id_A(x,y)\,:\,\mathrm{Type}}}$ |
Under Curry-Howard we understand $Id_A(x,y)$ as the proposition $x=y$.
| ${\large\frac{\dots\ \vdash\ \dots}{\dots\ \vdash\ refl_x\,:\,Id_A(x,x)}}$ |
That's the reflexivity postulate $x=x$.
| ${\large\frac{\dots,\,p\,:\,Id_A(x,y)\ \vdash\ Q(x,y,p)\,:\,\mathrm{Type}\hspace{.5cm}\dots\ \vdash\ t\,:\,Q(x,x,refl_x)}{\dots\ \vdash\ J(t,x,y,p)\,:\,Q(x,y,p)}}$ |
This means that if we know that $x=y$, then if $Q(x,x)$ is true, then so must be $Q(x,y)$.
| $J(t,x,x,refl_x):=t$ |
The terms of this type behave like paths between the terms $x,y$. Under the propositions as type paradigm, these can be considered proofs of equality of $x$ and $y$.
The path object interpretation “$A^I$” (in quotes because there need to be no interval and this isn't an exponential object) is suitable in intensional type theory, where there might be many terms of $Id_A$. In an extensional theory (or when one deals with mere proposition) where only yes/no counts, $Id_U$ has the semantics of the diagonal relation $\Delta_A$ on $A\times A$
One might denote the identity type by $Path_A(x,y)$ or $x=_Ay$. If the context is given, then one might write $x=y$.
For example, since $+:{\mathbb N}\to{\mathbb N}\to{\mathbb N}$ we might ask if the types
$2+2=_{\mathbb N}5$
or
$2+3=_{\mathbb N}5$
are inhabited.
Defining hom-classes $A[x,y]:=Id_A(x,y)$ makes a type $A$ into a groupoid (a category with all arrows invertible). In fact it's an $\infty$-groupoid since if $q,p:Id_A(x,y)$, then $Id_{Id_A(x,y)}(p,q)$ is a type too.
In this wiki I use
| $\equiv$ … intensional equality (definitions) |
$myPair\equiv\langle 3,4\rangle$
| $:=$ … intensional equality for functional objects (function definitions) |
$\pi_1(\langle a,b\rangle):=a$
$f(x):=x+10$
| $=$ … propositional equality (derived or postulated statements) |
$f(\pi_1(\langle 3,4\rangle))=13$
| $=_A$ … identity type (propositional equality in the object language) |
| $\cong$ … isomorphism |
| $\simeq$ … equivalence |
There is a correspondence between a predicate $P$ over a class of objects and it's extension $\{x\ |\ P(x)\}$. The latter is the collection of objects it describes.
The predicates “$x$ is a natural number bigger than $1$ and smaller than $4$” and “$x$ is one of the first two prime numbers” have the same extension. The precise way of how a predicate is formulated is its intension.
We see that intensionally different definition can have the same extension.
We have $2(12+15)=2*3*4+2*3*5=3(8+10)$, and while $2(12+15)\mapsto 24+30$ and $3(8+10)\mapsto 24+30$ feel like natural reductions, $2(12+15)\mapsto 3(8+10)$ feels random. That is to say, there is a sort of computational direction that comes with a formulized evaluation.
nLab: canonical form
Now different frameworks have differnt capabilities of formally recognizing intension/extension. Without any context, let's write
$f:{\mathbb N}\to{\mathbb N}$
$f(n):=2\cdot(n+5)$
$g:{\mathbb N}\to{\mathbb N}$
$g(n):=2\cdot n+10$
This is supposed to be the definition of two functions $f$ and $g$ and they are a apriori intensionally different. (A more irl example would be two sorting algorithms, one efficiently, and one coded up so badly that it takes exponential time to compute.)
Now if the derivation rules of a theory are set up to realize function extensionality, then this means the only way to see equality of two functions is by application of argument. In this case we'd be able to show $\forall n.\,f(n)=g(n)$ and deriv $f=g$.
If the theory “is able to look at the code” then we'd be able see that they have different intension, while having the same extension. “Not seeing intension” is often good for doing mathematics, but not for studying how-properties in computer science.
nLab: identity type canonical form
StackExchange: Andrej Bauer on intentional equality