HoTTEST Summer School HoTT Notes 3

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

Two variable version

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

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

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

$$ \text{=-comp}: \require{bussproofs} \begin{prooftree} \AxiomC{$x:A, y:A, p:x\underset{A}{=} y \vdash D(x,y,p)\ 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} $$

Single variable version

$$ \text{=-form}: \require{bussproofs} \begin{prooftree} \AxiomC{$a:A$} \UnaryInfC{$x : A \vdash a \underset{A}{=} x\ type$} \end{prooftree} $$

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

$$ \text{=-elim}: \require{bussproofs} \begin{prooftree} \AxiomC{$a : A$} \AxiomC{$x : A, p : a\ {=_A}\ x ⊢ P(x, p)\ type$} \BinaryInfC{$ind_= : P(a, refl_a) \rightarrow \Pi_{(x:A)}{\Pi_{(p:a{=_A}x)} P(x, p)}$} \end{prooftree} $$

$$ \text{=-comp}: \require{bussproofs} \begin{prooftree} \AxiomC{$a : A$} \AxiomC{$x : A, p : a\ {=_A}\ x ⊢ P(x, p)\ type$} \BinaryInfC{$u : P(a, refl_a) \vdash ind_=(u, a, refl_a) : P(a, refl_a)$} \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 \underset{A}{=} b) \doteq (a \underset{A}{=} a)$, and

if $refl_a:a \underset{A}{=} a$ and $(a \underset{A}{=} b) \doteq (a \underset{A}{=} a)$, then $refl_a:a=_Ab$.

So we can internalize $a \doteq b : A$ with $refl_a:a\underset{A}{=}b$.

Functoriality¹

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\underset{A}{=}a' \rightarrow f\ a\underset{B}{=} f\ a' $$

Or in math language:

$$ ap: \Pi_{(f:A\rightarrow B)} \Pi_{(a,a':A)} a \underset{A}{=} a' \rightarrow b \underset{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\underset{B}{=} f\ a$} \UnaryInfC{$f:A\rightarrow B, a:A, a':A, p: a\underset{A}{=}a' \vdash ind_=(refl_{f\ a},a,a',p): f\ a \underset{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 \underset{A}{=} a' \rightarrow f\ a \underset{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\underset{A}{=} a$} \UnaryInfC{$a,b:A, p: a\underset{A}{=} b \vdash ind_=(refl_a,a,b,p):b\underset{A}{=} a$} \UnaryInfC{$\lambda a,b,p. ind_=(refl_a,a,b,p):\Pi_{(a,b:A)}a\underset{A}{=}b \rightarrow b\underset{A}{=}a$} \end{prooftree} $$

Composition of Equalities

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

The Space Interpretation of Types

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

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 equality 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\underset{B}{=}b'\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\underset{B}{=}b') \rightarrow E(b) \rightarrow E(b')$} \end{prooftree} $$

transport : ∀ {B : Set} (E : B → Set) {b b' : B}
            (p : b ≡ b') → E b → E b'
transport E refl = λ x → x

Materials

Lecture Note

HoTTEST_Lecture_3.pdf

Record on Youtube