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

Steve Awodey (Pittsburgh), Type theory of higher-dimensional categories. Abstract.
Benno van den Berg (Darmstadt), Types as weak omega-categories. Abstract.
Wojciech Chacholski (Stockholm), Representations of spaces and mapping complexes. Abstract.
Peter Dybjer (Göteborg), History and meaning of the identity type. Abstract.
Nicola Gambino (Montreal), Quillen model structures on diagrams of categories. Abstract.
Richard Garner (Uppsala), Factorisation systems for type theory. Abstract.
Martin Hyland (Cambridge), Algebraic homotopy theory: lessons for type theory. Abstract.
Maria Emilia Maietti (Padova) and Giovanni Sambin (Padova), Intensionality vs. extensionality: a solution with two levels of abstraction. Abstract.
Per Martin-Löf (Stockholm), Topos theory and type theory. Abstract.
Thomas Streicher (Darmstadt), Identity types vs. weak omega-groupoids: some ideas, some problems. Abstract.
Michael A Warren (Pittsburgh), Model categories and intensional identity types. Abstract.

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

Programme

The final programme is available here.

Organiser:

Erik Palmgren, Uppsala University

Venue

(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!]

Accomodation

is expected to be arranged by participants themselves. Here is a list of hotels (prices are subject to change).

November 8, 2006, Erik Palmgren.