Workshop on Identity Types

Workshop on Identity Types

[Erik Palmgren]

   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