Identity Types - Topological and Categorical Structure Workshop, November 13-14, 2006, Uppsala University. 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 his connection is intended to be the main theme of this workshop. Preliminary list of speakers Steve Awodey (Pittsburgh) Peter Dybjer (Göteborg) Richard Garner (Uppsala) Martin Hyland (Cambridge, to be confirmed) Per Martin-Löf (Stockholm) Thomas Streicher (Darmstadt) Michael A Warren (Pittsburgh) A final list of speakers will be prepared shortly before the workshop. If you are interested in giving a talk, please submit a short abstract to the organiser before October 25. The working days of the meeting are November 13 and November 14 until noon. Organiser: Erik Palmgren, Uppsala University, email: palmgren@math.uu.se Venue: Uppsala University, Polacksbacken, Lägerhyddsvägen 1-2, Uppsala, Sweden. Accomodation is expected to be arranged by the participants themselves. See the workshop webpage for a list of recommended hotels and further information. Workshop webpage: www.math.uu.se/~palmgren/itt
participants (1)
-
Erik Palmgren