Skip to content

Simplicial HoTT and synthetic ∞-categories

Info

This project originated as a fork of emilyriehl/yoneda.

This is a formalization library for simplicial Homotopy Type Theory (sHoTT) with the aim of proving resulting in synthetic ∞-category theory, starting with the results from the following papers:

This formalization project follows the philosophy laid out in the article "Could ∞-category theory be taught to undergraduates?" 4.

The formalizations are implemented using rzk, an experimental proof assistant for a variant of type theory with shapes.

See the list of contributors to this formalisation project at CONTRIBUTORS.md.

Checking the formalisations locally

It is recommended to use VS Code extension for Rzk (available in Visual Studio Marketplace, as well as in Open VSX). The extension should then manage an rzk executable and provide some feedback directly in VS Code, without users having to use the command line.

Otherwise, install the rzk proof assistant from sources. Then run the following command from the root of this repository:

rzk typecheck src/hott/* src/simplicial-hott/*

  1. Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures 1(1), 147-224. 2017. https://arxiv.org/abs/1705.07442 ↩

  2. Ulrik Buchholtz and Jonathan Weinberger. Synthetic fibered (∞, 1)-category theory. Higher Structures 7 (2023), 74–165. Issue 1. https://doi.org/10.21136/HS.2023.04 ↩

  3. César Bardomiano Martínez. Limits and colimits of synthetic ∞-categories. 1-33, 2022. https://arxiv.org/abs/2202.12386 ↩

  4. Emily Riehl. Could ∞-category theory be taught to undergraduates? Notices of the AMS. May 2023. https://www.ams.org/journals/notices/202305/noti2692/noti2692.html ↩