Papers With

← All papers
First page of Formalization of Non-Abelian Topology for Homotopy Type Theory

Formalization of Non-Abelian Topology for Homotopy Type Theory

Jakob von Raumer

cs.LO Jan 1, 2015 · v1
formalization topology type-theory
Read PDF arXiv abstract
TL;DR
Formalizes non-abelian algebraic topology constructions in Lean within a HoTT framework.
Abstract
This thesis develops non-abelian algebraic topology within the framework of homotopy type theory, formalized in the Lean proof assistant. It establishes constructions involving higher groupoids and their relationship to homotopy types, extending the computational content of homotopy type theory beyond abelian structures. The formalization demonstrates how dependent type theory provides a natural setting for higher-dimensional algebraic topology.
Problem

Non-abelian algebraic topology extends homotopy type theory beyond abelian structures, but formalizing higher groupoids and their relationship to homotopy types in a proof assistant had not been done.

Approach

The thesis develops non-abelian algebraic topology within the framework of homotopy type theory, formalized in Lean. It establishes constructions involving higher groupoids and their relationship to homotopy types, using dependent type theory as the setting for higher-dimensional algebraic topology.

Results

The formalization demonstrates that dependent type theory provides a natural setting for higher-dimensional algebraic topology, extending the computational content of homotopy type theory to non-abelian structures with machine-checked constructions of higher groupoids.