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!

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:

Feel free to organize a group, and to add more suggestions!