Thomas Streicher

April 16, 2016
  1. April 2016
Isomorphic Types are Equal?

Identity types in Martin-Löf type theory are an intriguing concept and a bit cumbersome to use. In particular, an identity type Id(A,a,b) may contain more than one element. These difficulties are compensated by the fact that for universes U identity on U may be considered as isomorphism, i.e. for A,B in U the identity type Id(U,A,B) is isomorphic to the type of isomorphisms between A and B.

This has been first spotted in the groupoid model of M. Hofmann and myself in 1993. Around 2006 this has been observed by V. Voevodsky for the simplicial set model where types are interpreted as Kan complexes, i.e. weak higher dimensional groupoids and the above axiom has been called “Univalence Axiom” by him.

We will explain the basic concepts and will sketch the construction of the simplicial set model. The latter is well known and in common use in modern homotopy theory where spaces are studied in terms of their associated weak higher dimensional groupoids.

Slides are available here.