Paolo Capriotti abstract and references

Title: (∞,1)-categories in Homotopy Type Theory

Abstract: We will look at some ideas on how to extend the classical model of(∞,1)-categories given by complete Segal spaces to the setting ofHomotopy Type Theory (HoTT). Since the category Δ is not direct, we are forced to replace bisimplicial sets with semi-simplicial types, which means that categorical identities cannot be immediately recovered from degeneracies.  However, somewhat surprisingly, a notion of completeness can be defined for semi-Segal types, and it seems to be possible to develop a satisfactory theory of (n,1)-categories based on complete semi-Segal types internally in HoTT.


Univalence for inverse diagrams and homotopy canonicity

Univalent categories and the Rezk completion

Quasi-unital ∞-Categories

Concrete Categories in Homotopy Type Theory

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.