Working groups in several different areas are being organized by participants.
We currently have two active working groups:
Coq: all aspects of UF in Coq. Meets Wednesdays 1:30 - 3 in S101. Organized by Andrej Bauer wiki page
Informal HoTT. Meets Tuesdays 1:30 - 3 in S101. Organized by Peter Aczel wiki page
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!
Created on April 19, 2018 at 21:16:58
by
Univalent foundations special year 2012