Identity type

Type

In the following I write “$\dots$” for some formal necessary context declarations, but which don't help understanding the rules.

Type introduction rule
${\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$.

Term introduction rule
${\large\frac{\dots\ \vdash\ \dots}{\dots\ \vdash\ refl_x\,:\,Id_A(x,x)}}$

That's the reflexivity postulate $x=x$.

Term elimination
${\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)$.

Computational rule
$J(t,x,x,refl_x):=t$
Interpretation

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$

Notation

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$.

Example

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.

Rules

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.

On AoC

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

Intension, extension

See Andrej Bauer on intentional equality

The concept

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.

Canonical form, canonicity of formal systenms)

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

In theories

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.

Reference

nLab: identity type canonical form

StackExchange: Andrej Bauer on intentional equality

Parents

Dependent type theory