Posted in

Speaker:

Thomas Streicher
Date:

Sat, 13/02/2016 - 16:30 - 18:00
Location:

MPIM Lecture Hall
Parent event:

Workshop on Homotopy Type Theory In old work by Martin Hofmann (CSL 1994) he used Giraud's right adjoint

splitting for splitting locally cartesian closed categories in order to

make them ready for interpreting the syntax of MLTT. He observed that

there were problems with extending this work to impredicative universes

as in Ehrhard's dictoses (a notion of model for Calculus of

Constructions).

I will describe recent attempts based on different methods of splitting

models. I will try to pinpoint where they fail and will isolate the key

problem, namely that splitting small universes may make them big.

© MPI f. Mathematik, Bonn | Impressum & Datenschutz |