Welcome to the wiki of the special year on Univalent Foundations of Mathematics 2012/2013 at the Institute for Advanced Study in Princeton, NJ, coorganized by Steve Awodey, Thierry Coquand and Vladimir Voevodsky.

This wiki contains various material relevant to this special program.

**Note:** Now that the special program is over, there is a new wiki dedicated to the *subject* of homotopy type theory and univalent foundations, which should be used instead of this one (and content migrated over as possible). It can be found here.

You are currently viewing a non-editable archival copy of the original UF program wiki that was made when the original Wikispaces provider closed down in 2018.

A list of the participants to the special year is available at IAS program participants

On an average week we have

- A tutorial on Monday evening, see Tutorials
- A working group on informal type theory on Tuesday afternoon, see Informal Type Theory and The book
- Two seminars on Wednesday and Thursday morning, see Seminar
- A working group on Coq on Wednesday afternoon, see Coq Working Group
- An additional seminar on Friday morning, see Seminar

See Working Groups for more general informations on the working groups.

An up-to-date Google Calendar is available at Calendar.

Note: the seminars are sometimes recorded and the videos are available here: http://video.ias.edu/sm.

Notes from the final organizational meeting.

Notes, code, slides, references and resources are listed in the following pages (in alphabetical order), don’t hesitate to add relevant resources.

- Definitional Equality
- Higher Inductive Types
- Logical Frameworks
- Meaning Explanations
- Modal type theory
- Resources
- Semantics of type theory
- Setoid model of type theory formalized
- Setoids, Groupoids, etc
- Universes

- Description of some open problems about HoTT and of some theorems in homotopy theory that we should try to formalize in HoTT, see Open Problems
- One famous open problem about HoTT is the formalization of (semi-)simplicial type, see Semi-simplicial types
- Outline of the type system underlying the project of a new proof assistant, see Outline of the proof assistant
- Some relevant links

This wiki is set to “protected” mode which means that everyone can read everything but only members of the wiki can edit pages. Even without being a member of the wiki one can create a “discussion post” on any page. To do it press the button to the right from the “Edit” button in the top right area of the page and then the “new post” button.

To request membership please click “Join” (or, if you have a Wikispaces account, “Sign in”) button located in the right upper corner of the window and follow the instructions provided there. In order for your request to be approved your real name should either be clear from your login name or be available on your Wikispaces profile page.

You can see everything that has been added or changed on the wiki since your last visit at Recent Changes. *[Note: This is no longer true, as this is an archival copy of the wiki]*

Revised on May 4, 2018 at 08:23:10
by
Mike Shulman