Homotopy Type Theory HomePage (Rev #47, changes)

Showing changes from revision #46 to #47: Added | Removed | Changed

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
• The Homotopy Type Theory book

As of 6 June 2022, the HoTT web is regarded as deprecated. All further HoTT-related editing should happen on the main nLab web, and anyone who feels like porting an entry or two from there to here would do a great service to the community.

Some important pages on this wiki are:

• About this wiki
• Open problems
• Synthetic homotopy theory
• A list of Formalized Homotopy Theory
• Large types in HoTT
• Category theory in HoTT
• Higher algebra in HoTT
• Logic in HoTT
• Analysis in HoTT
• Number theory in HoTT
• Topology in HoTT
• Differential geometry in HoTT
• 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:

• A 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

Some forums:

• Homotopy Type Theory Google Group For current research.
• HoTT Cafe Google Group “A place where non-experts can discuss homotopy type theory and related topics. Experts are welcome to join in of course!”
• HoTT Zulip Chat “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.”
• nForum

If you have any ideas for articles that you would like to see, let us know!

• desired articles