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 [wiki page]
2. Informal HoTT. Meets Tuesdays 1:30 - 3 in S101. Organized by Peter Aczel [wiki page]
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!