Synthetic Homology in Homotopy Type Theory

2017/06/05 by R. L. Graham, Graham, Robert · 1 citation
Computer Science · Mathematics · #Algebraic structures and combinatorial models #FOS: Computer and information sciences #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Logic in Computer Science (cs.LO) #Topological and Geometric Data Analysis

paper · pdf · doi:10.48550/arxiv.1706.01540

openalex publication_date 2017/06/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• The Simplicial Model of Univalent Foundations (after Voevodsky)

Cited by

• On the Formalization of Higher Inductive Types and Synthetic Homotopy\n Theory

Related

• Classifying Types
• Synthetic Homotopy Theory
• On the Formalization of Higher Inductive Types and Synthetic Homotopy\n Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Homotopy type theory: the logic of space