Skip to content
forked from rzk-lang/sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

Notifications You must be signed in to change notification settings

jonalfcam/sHoTT

 
 

Repository files navigation

Simplicial HoTT and synthetic ∞-categories

Check 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 layed out in the article "Could ∞-category theory be taught to undergraduates?" [3].

The formalizations are implemented using rzk, an experimental proof assistant for a variant of type theory with shapes. Formalizations were contributed by Fredrik Bakke, Nikolai Kudasov, Emily Riehl, and Jonathan Weinberger.

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 src/hott/* src/simplicial-hott/*

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

Languages

  • JavaScript 52.4%
  • CSS 47.6%