Identity Types - Topological and Categorical Structure

Workshop, Uppsala, November 13-14, 2006

(Ångström laboratory, Uppsala University)

Theme of workshop

The identity type, the type of proof objects for the fundamental propositional equality, is one of the most intriguing constructions of intensional dependent type theory (also known as Martin-Löf type theory). Its complexity became apparent with the Hofmann-Streicher groupoid model of type theory. This model also hinted at some possible connections between type theory and homotopy theory and higher categories. Exploration of this connection is intended to be the main theme of the workshop.

List of speakers

The working days of the meeting are Monday November 13, and November 14 until noon.


The final programme is available here.


Erik Palmgren, Uppsala University


(Building 6, 7, 63 and 3 in the MIC area. Photo by Roland Grönroos)

Uppsala University, Polacksbacken, Lägerhyddsvägen 1-2, Uppsala. The workshop will be held on two different but nearby locations. It starts in the morning of November 13, in room 6140, which is situated in Building 6 in the MIC area. The entrance is between building 5 and 6 and has a sign "Aula" next to it. See map. After the lunch break the workshop continues in room Å4004, located in the Ångström laboratory building across the street (Lägerhyddsvägen). Å4004 is on the ground floor of building 4 ("hus 4"). See this map of the laboratory. The entrance from the street is at the top of the map. The location for the final morning session on November 14 is again room 6140.

Instructions how to get to Uppsala. [Note that the information is reused from an old conference!]


is expected to be arranged by participants themselves. Here is a list of hotels (prices are subject to change).
November 8, 2006, Erik Palmgren.