Welcome to the Homotopy Type Theory wiki! This wiki-site is for collaborative work on homotopy type theory. If you are new to these subjects, you may want to check out: * The [Homotopy Type Theory web site](http://homotopytypetheory.org) * The [Homotopy Type Theory Google Group](https://groups.google.com/forum/#!forum/homotopytypetheory) * The [HoTT Cafe Google Group](https://groups.google.com/forum/#!forum/hott-cafe) * The [HoTT Zulip Chat](https://hott.zulipchat.com) --- > As of 6 June 2022, the HoTT web is regarded as deprecated. All further HoTT-related editing should happen on the main [[nLab:HomePage|nLab web]], and anyone who feels like porting an entry or two from there to here would do a great service to the community. When porting entries over to the nLab, please make adjustments to the material so that it makes sense in the larger context of the nLab, instead of blindly copying the material over. --- Some important pages on this wiki are: * [[About]] this wiki * [[Higher algebra]] * [[higher observational type theory]] * [[Large types in HoTT]] * [[Rational homotopy theory]] * [[Order theory]] * [[Logic]] * [[Analysis]] * [[Number theory]] * [[Topology]] * [[Differential geometry]] * a list of [[Libraries]] and [[Proof Assistants]] * the [[Resources]] page * the [[References]] page * the [[Sandbox]] page * [[articles that should be ported to the nLab]] Other important links: * [[Events]] collects programs, slides, and other resources of homotopy type theory workshops, meetings, and other events. * [nForum](https://nforum.ncatlab.org/) category: navigation