Homotopy Type Theory

Textbook: Homotopy Type Theory: Univalent Foundations of Mathematics.

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\).