Skip to main content
Try Wikispaces Classroom now.
Brand new from Wikispaces.
Pages and Files
Categorical Semantics WG
Coq for UF
Coq Working Group
Formalized Homotopy Theory
Higher Inductive Types
Homotopy Type System
how to add a plugin
IAS program participants
Informal Type Theory
Math in HoTT
Modal type theory
Notation and terminology
Add "All Pages"
Working groups in several different areas are being organized by participants.
We currently have two active working groups:
1. Coq: all aspects of UF in Coq. Meets Wednesdays 1:30 - 3 in S101. Organized by Andrej Bauer [
2. Informal HoTT. Meets Tuesdays 1:30 - 3 in S101. Organized by Peter Aczel [
3. Homotopy in Type Theory. Meets Thursdays 1:30 - 3 in Simonyi common room or seminar room.
We have also reserved S101 for Fridays 1 - 12:30, which can be used for additional meetings -- talk to Steve to organize a meeting.
Watch the google calendar for specific meeting times and places.
Some further proposed areas for working groups are:
Designing a new proof assistant
Correctness of the new proof assistant
Syntax, properties, and computational behavior of homotopy type theories
Semantics of homotopy type theory (with the Univalence Axiom, Higher Inductive Types, etc.)
Developing homotopy theory in type theory
Homotopy theory in type theory with nonclassical axioms (e.g. motivated by higher-categorical semantics)
Doing and speaking about mathematics informally in homotopy type theory
Feel free to organize a group, and to add more suggestions!
help on how to format text
Turn off "Getting Started"