Category Archives: Homotopy Theory

Spectral Sequences

Last time we defined cohomology in homotopy type theory; in this post I want to construct the cohomological Serre spectral sequence of a fibration (i.e. a type family). This is the second part of a two-part blog post. The first … Continue reading

Posted in Homotopy Theory | 19 Comments

Cohomology

For people interested in doing homotopy theory in homotopy type theory, Chapter 8 of the HoTT Book is a pretty good record of a lot of what was accomplished during the IAS year. However, there are a few things it’s … Continue reading

Posted in Homotopy Theory, Models | 18 Comments

The HoTT Book

This posting is the official announcement of The HoTT Book, or more formally: Homotopy Type Theory: Univalent Foundations of Mathematics The Univalent Foundations Program, Institute for Advanced Study The book is the result of an amazing collaboration between virtually everyone involved … Continue reading

Posted in Foundations, Higher Inductive Types, Homotopy Theory, Paper, Univalence | 3 Comments

Homotopy Theory in Type Theory: Progress Report

A little while ago, we gave an overview of the kinds of results in homotopy theory that we might try to prove in homotopy type theory (such as calculating homotopy groups of spheres), and the basic tools used in our synthetic approach … Continue reading

Posted in Higher Inductive Types, Homotopy Theory | 13 Comments

Covering Spaces

Covering spaces are one of the important topics in classical homotopy theory, and this post summarizes what we have done in HoTT.  We have formulated the covering spaces and (re)proved the classification theorem based on (right) -sets, i.e., sets equipped with … Continue reading

Posted in Code, Higher Inductive Types, Homotopy Theory | 5 Comments

Homotopy Theory in Homotopy Type Theory: Introduction

Many of us working on homotopy type theory believe that it will be a better framework for doing math, and in particular computer-checked math, than set theory or classical higher-order logic or non-univalent type theory. One reason we believe this … Continue reading

Posted in Applications, Higher Inductive Types, Homotopy Theory, Uncategorized, Univalence | 3 Comments