Christian Sattler abstract

We try to give a categorical overview of recent work, mostly going back to Coquand and coworkers, enabling constructive homotopical interpretations of type theory in certain presheaf categories. Crucially, dependent types are interpreted as uniform fibrations, the right class in an algebraic weak factorization system. We will focus in particular on the issues of dependent products and univalent universes, giving a categorical account of the so-called glueing construction involved in the latter.

Share this page:

Contact details

Department of Mathematics
University of Leicester
University Road
Leicester LE1 7RH
United Kingdom

Tel.: +44 (0)116 229 7407

Campus Based Courses

Postgraduate Taught:

Postgraduate Research:

Distance Learning Course  

Actuarial Science:

DL Study

Student complaints procedure

AccessAble logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has detailed accessibility guides for College House and the Michael Atiyah Building.