pith. sign in

arxiv: 1808.10690 · v1 · pith:BTUES3LCnew · submitted 2018-08-31 · 🧮 math.AT · cs.LO· math.LO

On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory

Floris van Doorn This is my paper
classification 🧮 math.AT cs.LOmath.LO
keywords homotopytheorysyntheticassistantatiyah-hirzebruchbeencohomologyconstruction
0
0 comments X
read the original abstract

The goal of this dissertation is to present synthetic homotopy theory in the setting of homotopy type theory. We will present various results in this framework, most notably the construction of the Atiyah-Hirzebruch and Serre spectral sequences for cohomology, which have been fully formalized in the Lean proof assistant.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Automating Boundary Filling in Cubical Type Theories

    cs.LO 2024-02 conditional novelty 7.0

    Presents solvers for contortion (via poset maps for Dedekind/De Morgan) and Kan problems (via CSP) in cubical type theory, implemented in Haskell and demonstrated on Eckmann-Hilton.