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]] * [[Higher algebra in HoTT]] * [[Analysis in HoTT]] * a list of [[Libraries]] and [[Proof Assistants]] * the [[Resources]] page * the [[References]] page * the [[Sandbox]] page Discussion about the wiki occurs at the [nForum](https://nforum.ncatlab.org/). 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 forums: * [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!" * [HoTT Zulip Chat](https://hott.zulipchat.com) "A friendly and relaxed place for online discussions about anything related to homotopy type theory. We discuss both formal and informal approaches, and we work with Coq, Agda, Cubical TT, and other systems." If you have any ideas for articles that you would like to see, let us know! * [[desired articles]] 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