Identity Types

In intensional type theory under the propositions as types paradigm, an identity type (or equality type) is the incarnation of equality. That is, for any type $A$ and any terms $x,y:A$, the type $Id_A(x,y)$ is “the type of proofs that $x=y$” or “the type of reasons why $x=y$”. —— nLab

Judgemental Equality vs Propositional Equality

Judgemental equality, or definitional equality since we won't pay much attention to the difference in this course, is intensional equality, or equality of meaning (synonymy). Or in words understandable for normal human beings, definitional equality is something equals to another thing "magically", they are equal to each other just because we SAY IT.

For example, in all the rules mentioned in past several notes and proofs built by these rules, we use judgemental equality $\doteq$.

As we all see, there are many terms which are judgmental equal and we can prove them, but there're also some terms which "should" be equal but we cannot prove, eg. we cannot find a proof for $add(0, x) \doteq x$, and that's where propositional equality and identity types come for help, which basically is a type which stands for "equal".

Type Constructors Often Internalize Structure

(Don't really get what the teacher want to show by saying these.)

Maybe used to show that types are used to describe some certain property of something, so we can think identity types internalize the property that something is propositional equal to another thing.

Rules on Identity Types

$$ =-form: \require{bussproofs} \begin{prooftree} \AxiomC{$A\ type\ a:A\ b:A$} \UnaryInfC{$a=_A b\ type$} \end{prooftree} $$

$$ =-intro: \require{bussproofs} \begin{prooftree} \AxiomC{$a:A$} \UnaryInfC{$refl_a : a=_A a\ type$} \end{prooftree} $$

$$ =-elim: \require{bussproofs} \begin{prooftree} \AxiomC{$x:A, y:A, z:x=_A y \vdash D(x,y,z)\ type$} \AxiomC{$x:A \vdash d:D(x,x,refl_x)\ type$} \BinaryInfC{$x:A, y:A, z:x=_A y \vdash ind_=(d,x,y,z) : D(x,y,z)\ type$} \end{prooftree} $$

$$ =-comp: \require{bussproofs} \begin{prooftree} \AxiomC{$x:A, y:A, z:x=_A y \vdash D(x,y,z)\ type$} \AxiomC{$x:A \vdash d:D(x,x,refl_x)\ type$} \BinaryInfC{$x:A \vdash ind_=(d,x,x,refl_x) \doteq d: D(x,x,refl_x)$} \end{prooftree} $$

Reflexivity

We can use $refl_x$ to internalize (or "downgrade", if you prefer human being's language) judgmental equality to propositional equality, ie.

Since we have

If $a \doteq b : A$, then $(a =_A b) \doteq (a =_A a)$, and

if $refl_a:a =_A a$ and $(a =_A b) \doteq (a =_A a)$, then $r_a:a=_Ab$.

So we can internalize $a \doteq b : A$ with $r_a:a=_Ab$.

Functoriality1

Functoriality means that something is a functor. e.g. when someone asks about the functoriality of some construction, they're asking whether or not it can be upgraded to a functor. —— stackexchange problem

So basically it is the property of whether a construction is a functor.

Arrrrgh, functor, another classical Haskell thing.

In functional programming, a functor is a design pattern inspired by the definition from category theory, that allows for a generic type to apply a function inside without changing the structure of the generic type. —— Wikipedia

Or, functors are functions act on paths/terms of the identity type.

For any two types $A$, $B$, any function $f:A\rightarrow B$, and any two terms $a:A, a':A$, there exists a functor: $$ ap_f: a=_Aa' \rightarrow f\ a=_B f\ a' $$

Or in math language:

$$ ap: \Pi_{(f:A\rightarrow B)} \Pi_{(a,a':A)} a =_A a' \rightarrow b =_A b' $$

We can prove this by using $=-elim$ rule.

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$f:A\rightarrow B, a:A \vdash refl_{f\ a}:f\ a=_B f\ a$} \UnaryInfC{$f:A\rightarrow B, a:A, a':A, p: a=_Aa' \vdash ind_=(refl_{f\ a},a,a',p): f\ a =_B f\ a' $} \UnaryInfC{$\lambda f. \lambda a.\lambda a'. ind_=(refl_{f\ a},a,a',p):\Pi_{(f:A\rightarrow B)} \Pi_{(a,a':A)} a =_A a' \rightarrow f\ a =_B f\ a'$} \end{prooftree} $$

Proof Example

Prove: $\Pi_{(n:\mathbb N)} add(0,n) = n$.

You can use the following two judgemental equality rules, which is provable before we have $refl$ or such things: $$ add(n, 0) \doteq n $$

$$ add(n, succ(m)) \doteq succ(add(n, m)) $$

We start as normal:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$$} \UnaryInfC{$?:\Pi_{(n:\mathbb N)} add(0,n)=n$} \end{prooftree} $$

Then let's use $\Pi-intro$:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$n:\mathbb N \vdash ?:add(0,n)=n$} \UnaryInfC{$?:\Pi_{(n:\mathbb N)} add(0,n)=n$} \end{prooftree} $$

Then $\mathbb N-elim$:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$?: add(0,0)=0$} \AxiomC{$n:\mathbb N, p: add(0, n)=n \vdash ?: add(0,succ(n))=succ(n)$} \BinaryInfC{$n:\mathbb N \vdash ?:add(0,n)=n$} \UnaryInfC{$?:\Pi_{(n:\mathbb N)} add(0,n)=n$} \end{prooftree} $$

For $add(0,0)=0$, we can downgrade judgemental equal rule $add(n, 0) \doteq n$ where $n=0$ with $refl_0$.

For $add(0,succ(n))=succ(n)$, we can use $ap_{succ}$ on $p$:

$$ \displaylines { ap_{succ}: a=a' \rightarrow succ(a)=succ(a')\\ ap_{succ}\ p: (a=a' \rightarrow succ(a)=succ(a'))\ (add(0, n)=n) \\ ap_{succ}\ p: succ(add(0, n))=succ(n) } $$

Let's put them in:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$refl_0: add(0,0)=0$} \AxiomC{$n:\mathbb N, p: add(0, n)=n \vdash ap_{succ}\ p: add(0,succ(n))=succ(n)$} \BinaryInfC{$n:\mathbb N \vdash ?:add(0,n)=n$} \UnaryInfC{$?:\Pi_{(n:\mathbb N)} add(0,n)=n$} \end{prooftree} $$

And fill the holes:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$refl_0: add(0,0)=0$} \AxiomC{$n:\mathbb N, p: add(0, n)=n \vdash ap_{succ}\ p: add(0,succ(n))=succ(n)$} \BinaryInfC{$n:\mathbb N \vdash ind_{\mathbb N}(refl_0, ap_{succ}\ p, n):add(0,n)=n$} \UnaryInfC{$\lambda n. ind_{\mathbb N}(refl_0, ap_{succ}\ p, n):\Pi_{(n:\mathbb N)} add(0,n)=n$} \end{prooftree} $$

In agda, note ap is called cong in agda:

add-0-n :  (n : ) → 0 + n n
add-0-n zero = refl
add-0-n (suc n) = cong suc refl 

The Groupoidal Behaviour of Types

We can think terms as points, and we can use paths/homotopies which stands for identity to connect them.

connected

Here are three terms a, b and c, and a is proportional equal to b and b is proportional equal to c, which we represent with p and q.

And we can play freely with these terms and equals, eg.

  • We can have multiple equalities of the same type
  • We can take the inverse of an equality
  • We can take composition of equalities
  • We can have equalities of equalities

And that's how homotopies in space behave.

Proof of these properties

Inverse of an Equality

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$a:A\vdash refl_a:a=_A a$} \UnaryInfC{$a,b:A, p: a=_A b \vdash ind_=(refl_a,a,b,p):b=_A a$} \UnaryInfC{$\lambda a,b,p. ind_=(refl_a,a,b,p):\Pi_{(a,b:A)}a=_Ab \rightarrow b=_Aa$} \end{prooftree} $$

Composition of Equalities

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$a,c:A\vdash \lambda x.x: a=_Ac \rightarrow a=_A c$} \UnaryInfC{$a,b,c:A, p:a=_Ab \vdash ind_=(\lambda x.x, a, b,p):b=_Ac \rightarrow a=_Ac$} \UnaryInfC{$\lambda a,b,c,p. ind_=(\lambda x.x, a, b,p): \Pi_{(a,b,c:A)} a=_Ab \rightarrow b=_Ac \rightarrow a=_Ac$} \end{prooftree} $$

Composition of Equalities

The Space Interpretation of Types

There's an interpretation of dependent type theory into space (the category of Kan complexes2) in which:

Type theoryHomotopy theoryKan complexes
TypesSpacesKan complexes
TermsPoints0-Cells
EqualitiesPath fibration0-Cells of path object
$\pi: \Sigma_{(b:B)}E(b)\rightarrow B$Kan fibrations
$\pi: \Pi_{(b:B)}E(b)$The space of sections of $\pi: \Pi_{(b:B)}E(b)$
Dependent typesFibrations
Dependent pair typeTotal Space

Transport

For any dependent type $x:B\vdash E(B)\ type$, any terms $b,b':B$ and any equality $p:b=_Bb'$, there is a function $tr_B:E(b)\rightarrow E(b')$

Basically it means propositional qquality remains when apply some dependent type "over" it.

This is part of a more sophisticated relationship between type theory and homotopy theory (Quillen model category theory) Transport says that $\pi: \Sigma_{(b:B)}E(b)\rightarrow B$ behaves like a fibration in a QMC.

Proof

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$b:B\vdash \lambda x.x: E(b) \rightarrow E(b)$} \UnaryInfC{$b,b':B,p:b=_Bb'\vdash ind_=(\lambda x.x, b, b', p): E(b) \rightarrow E(b')$} \UnaryInfC{$\lambda b,b,p.ind_=(\lambda x.x, b, b', p): \Pi_{(b,b':B)}(b=_Bb') \rightarrow E(b) \rightarrow E(b')$} \end{prooftree} $$

1

The VSCode spell checker told me this is not even an existing word, and so do many mathematic terms in this article, mathematicians are really good at inventing terms!

2

WTF is that 😭 TODO: learn it.