# Homotopy Type Theory

## Introduction

### Homotopy

A homotopy between a pair of continuous maps $$f, g : X \to Y$$ is a continuous map $$H : X \times [0, 1] \to Y$$ satisfying $$H(x, 0) = f(x)$$ and $$H(X, 1) = g(x)$$.

### Homotopy equivalent / Homotopy type

Two spaces (not maps!) $$X, Y$$ are homotopy equivalent $$X \simeq Y$$ if there exist a pair of mappings between them $$f : X \to Y, g : Y \to X$$ such that there exists a homotopy between:

• $$f \cdot g$$ and the identity function of $$X$$.
• $$g \cdot f$$ and the identity function of $$Y$$.

Intuitively, the two spaces are isomorphic to each other up to a homotopy.

If $$X \simeq Y$$, we say they have the same homotopy type.

### Universe

A type whose elements are themselves types. Denoted by $$\mathcal{U}$$.

### Univalence axiom

$(X = Y) \simeq (X \simeq Y)$

In other words, there exists a homotopy equivalence between the type of identity and of equality. Identity is equivalent to equivalence.

## Part 1: Foundations

### Chapter 1: Type theory

#### 1.3 Universes and families

##### Hierarchy of universes

$\mathcal{U}_0 : \mathcal{U}_1 : \mathcal{U}_2 : ...$

Universes are cumulative.

##### Small type

When a universe $$\mathcal{U}$$ is assumed, elements of it are called small types.

##### Codomain

For a function $$f: X \to Y$$, $$Y$$ is the codomain.

N.B.: It’s not the elements of $$Y$$ that $$f$$ maps onto, it’s the whole of $$Y$$.

##### Family of types

$B : A \to \mathcal{U}$

where $$B$$ is the family. For example, $$\text{Fin} : \mathbb{N} \to \mathcal{U}$$ is the family of all finite sets of natural numbers.

#### 1.4 Dependent function types

##### Dependent functions

$\Pi_{(x : A)} B(x) : \mathcal{U}$

A function where its codomain depends on the element of the domain of its input (the type of the output depends on the input).

##### Polymorphic functions

A type of dependent function which takes a type as one of its arguments, and then acts on elements of that type.

For example, identity:

$id : \Pi_{(A : \mathcal{U})} A \to A$

#### 1.5 Product types

##### Cartesian product

$A \times B$

Consists of pairs $$(a, b) : A \times B$$.

##### Unit type

Consists of a single element:

$* : \mathbf{1}$

##### Recursors

For example, for the product type:

$\text{rec}_{A \times B} : \Pi_{C : \mathcal{U}} (A \to B \to C) \to (A \times B) \to C$

Defines a way of operating over the deconstructed elements of a type.

##### Induction

For example, for the product type:

$\text{ind}_{A \times B} : \Pi_{A : A \times B \to \mathcal{U}} ( \Pi_{x : A} \Pi_{y : B} C((x, y)) ) \to \Pi_{x : A \times B} C(x)$

Allows us to prove by induction for the $$A \times B$$ type.

#### 1.6 Dependent pair types ($$\Sigma$$-types)

A pair where the type of the second element depends on the value of the first.

$\Sigma_{x : A} B(x)$

where $$A : \mathcal{U}$$, $$B : A \to \mathcal{U}$$.

##### For-all, there-exists interpretation

We can read $$\Pi$$ as for-all, and $$\Sigma$$ as there-exists.

##### Magma

A magma is a type with a closed binary operator. We can express it using dependent pair types:

$\Sigma_{A : \mathcal{U}} A \to A \to A$

#### 1.7 Coproduct types

$A + B$

The union over $$A$$ and $$B$$.

#### 1.11 Propositions as types

##### Negation

$¬A : \equiv A \to \mathbf{0}$

Where $$\mathbf{0}$$ is a type that can not be populated.

##### Law of excluded middle (LEM)

We can’t use LEM in type theory. This means we can’t prove things like:

$((A \times B) \to \mathbf{0}) \to (A \to \mathbf{0}) + (B \to \mathbf{0})$

or

$((A \to \mathbf{0}) \to \mathbf{0}) \to A$

##### Semigroup

$\text{Semigroup} :\equiv \Sigma_{A : \mathcal{U}} \Sigma_{m : A \to A \to A} \Pi_{x, y, z : A} m(x, m(y, z)) = m(m(x, y), z)$

##### Logical equivalence

$(A \to B) \times (B \to A)$

e.g. $$\mathbb{N}$$ and $$\mathbf{1}$$ are logically equivalent.

#### 1.12 Identity types

##### Identity type

$\text{Id}_A : A \to A \to \mathcal{U}$

$$\text{Id}_A(x, y)$$ is the type representing equality between $$x$$ and $$y$$.

Also written as $$x =_A y$$, or $$x = y$$.

##### Reflexivity

$refl : \Pi_{a : A} (a =_A a)$

Constructor for identity types.

##### Indiscernibility of identities

For every family

$C : A \to \mathcal{U}$

There exists a function

$f : \Pi_{x, y : A} \Pi_{p : x=y} C(x) \to C(y)$

Such that

$f(x, x, \text{refl}_x) : \equiv id_{C(x)}$

##### Path induction

$\text{ind}_{=_A} : \Pi_{C : \Pi_{x, y : A} (x = y) \to \mathcal{U}} (\Pi_{x : A} C(x, x, \text{refl}_x)) \to \Pi_{x, y : A} \Pi_{p : x=y} C(x, y, p)$

States that: For a proposition $$C$$ that depends on the identity of two types, if we can prove it for reflexivity, it is true for non-reflexively equal elements.

Traditionally called $$J$$.

##### Based path induction

Like path induction, but with a fixed starting point $$a$$ in place of $$x$$.