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 book](http://homotopytypetheory.org/book) Some important pages on this wiki are: * [[About]] this wiki * [[Open problems]] * [[Synthetic homotopy theory]] * A list of [[Formalized Homotopy Theory]] * [[Category theory in HoTT]] * [[type theory]] * a list of [[Libraries]] and [[Proof Assistants]] * the [[Resources]] page * the [[References]] page Other important links: * A [calendar](https://github.com/UniMath/UniMath/wiki/Homotopy-type-theory-and-univalent-foundations-calendar) of HoTT/UF events maintained at the UniMath github wiki * [[Events]] collects programs, slides, and other resources of homotopy type theory workshops, meetings, and other events. Archived version of the now defunct UF-IAS wiki: * The [IAS UF program wiki](https://ncatlab.org/ufias2012/published/HomePage) Some mailing lists: * [Homotopy Type Theory Google Group](https://groups.google.com/forum/#!forum/homotopytypetheory) For current research. * [HoTT Cafe Google Group](https://groups.google.com/forum/#!forum/hott-cafe) "A place where non-experts can discuss homotopy type theory and related topics. Experts are welcome to join in of course!" For now, this wiki works in parallel to the n-Lab. Links to the nlab [[nlab:HomePage]] can be made using the prefix `nlab:` . For example, the pages that explain how to edit this wiki are the ones for the n-Lab's [[nlab:HowTo]]. category: navigation