Synthetic Homology in Homotopy Type Theory

TL;DR

This paper develops a framework for defining homology within homotopy type theory, enabling formal, computer-verified constructions of homological invariants and extending the synthetic approach to stable homotopy groups.

Contribution

It introduces a novel synthetic definition of homology in homotopy type theory, building on prior work in cohomology and establishing a foundation for computer-checked homological constructions.

Findings

Homology is formally defined within homotopy type theory.

Stable homotopy groups are also characterized in this framework.

Lays groundwork for automated, formal verification of homological properties.

Abstract

This paper defines homology in homotopy type theory, in the process stable homotopy groups are also defined. Previous research in synthetic homotopy theory is relied on, in particular the definition of cohomology. This work lays the foundation for a computer checked construction of homology.