## 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. 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 BKan 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.