Abstract Karol Szumilo

Internal Languages of Higher Categories

 Theory of (infinity, 1)-categories can be seen as an abstract framework for homotopy theory which emerged from classical category theory and algebraic topology. Homotopy Type Theory is a formal language originating from logic which can also be used to argue about homotopy theory. It is believed that HoTT is an "internal language" of (infinity, 1)-categories. Roughly speaking, this means that HoTT and higher category theory prove the same theorems. Even making this statement precise is challenging and leads to a range of conjectures of varying scope and depth. In this talk, I will discuss a proof of the simplest of these conjectures obtained in joint work with Chris Kapulkin.

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

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.