Description: A formalised, explorable online resource for Homotopy Type Theory.
categories (332) topos (48) agda (9)
module index where 1lab 🔗 A formalised, cross-linked reference resource for cubical methods in Homotopy Type Theory. Unlike the HoTT book , the 1lab is not a “linear” resource: Concepts are presented as a directed graph, with links indicating dependencies . For instance, the statement of the univalence principle depends on universes , identifications and equivalences . In addition to the hyperlinked “web of concepts” provided by the Agda code, there is a short introduction to homotopy type theory: Start her
The 1lab is a community project: we use GitHub for source control and talk on Discord . Our purpose is to make cubical methods in homotopy type theory accessible to, and inclusive of, everyone who is interested, regardless of cultural background, age, ability, ethnicity, gender identity, or expression. Correspondingly, interactions in those forums are governed by the Contributor Covenant Code of Conduct . We believe HoTT is for everyone, and are committed to fostering a kind, inclusive environment.
Mathematics is, fundamentally, a social activity. Correspondingly, we have a page dedicated to letting authors introduce and talk a bit themselves and their other work: