Synthetic Homotopy Theory

TL;DR

This dissertation develops synthetic homotopy theory within homotopy type theory, providing new synthetic constructions, proofs of fundamental theorems, and calculations of homotopy groups of spheres.

Contribution

It introduces synthetic constructions and proofs of key homotopy theorems using homotopy type theory, advancing the formalization of homotopy theory.

Findings

Synthetic construction of the Hopf fibration

Proof of the Blakers--Massey theorem

Calculation of homotopy groups of n-spheres

Abstract

The goal of this dissertation is to present results from synthetic homotopy theory based on homotopy type theory (HoTT). After an introduction to Martin-L\"of's dependent type theory and homotopy type theory, key results include a synthetic construction of the Hopf fibration, a proof of the Blakers--Massey theorem, and a derivation of the Freudenthal suspension theorem, with calculations of some homotopy groups of $n$-spheres.