Skip to content
/ sHoTT Public

Formalisations for simplicial HoTT and synthetic ∞-categories.

Notifications You must be signed in to change notification settings

rzk-lang/sHoTT

Repository files navigation

Simplicial HoTT and synthetic ∞-categories

Typecheck with latest Rzk MkDocs to GitHub Pages

ℹ️ This project originated as a fork of https://github.com/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 at src/CONTRIBUTORS.md.

The formalizations can be viewed as markdown files rendered at rzk-lang.github.io/sHoTT/ using syntax highlighting supplied by MkDocs plugin for Rzk.

Checking the formalisations locally

Install the rzk proof assistant. Then run the following command from the root of this repository:

rzk typecheck

Please also have a look at our style guide before submitting your pull request.

References

  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. 2023. 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

About

Formalisations for simplicial HoTT and synthetic ∞-categories.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published