Categorical structures for type theory in univalent foundations

Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)
47 Downloads (Pure)


In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in the setting of univalent foundations, where the relationships between them can be stated more transparently. Specifically, we construct maps between the different structures and show that these maps are equivalences under suitable assumptions. We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure. We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.
Original languageEnglish
Title of host publication26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
EditorsValentin Goranko, Mads Dam
PublisherSchloss Dagstuhl
ISBN (Print)9783959770453
Publication statusPublished - 1 Aug 2017
Event26th EACSL Annual Conference on Computer Science Logic (CSL 2017) - Stockholm, Sweden
Duration: 20 Aug 201724 Aug 2017

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl
ISSN (Electronic)1868-8969


Conference26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Abbreviated titleCSL 2017
Internet address


  • Categorical Semantics
  • Type Theory
  • Univalence Axiom


Dive into the research topics of 'Categorical structures for type theory in univalent foundations'. Together they form a unique fingerprint.

Cite this