Abstract Lumsdaine

Abstract:  It is widely believed that homotopy type theory should be the internal logic of elementary ∞-toposes — whatever that may mean.  I will present some recent progress (jww Chris Kapulkin) towards a precise statement and proof of this idea.
 Specifically, for various type theories, leading up to “full HoTT”, we assemble their models into an (∞,1)-category, with an ∞-functor to a suitable (∞,1)-category of structured (∞,1)-categories (e.g. LCCC_∞).  One may then conjecture that this ∞-functor is an equivalence — a precise and strong form of the “internal language” conjecture.
  The main technical tool used is the “Reedy span-equivalences” construction.  This turns out to also have applications of a more traditionally logical flavour, for equivalence and conservativity results between different type theories.

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

Undergraduate: mathsug@le.ac.uk
Postgraduate Taught: mathspg@le.ac.uk

Postgraduate Research: pgrmaths@le.ac.uk

Distance Learning Course  

Actuarial Science:

DL Study

Student complaints procedure

DisabledGo 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.