License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2017.8
URN: urn:nbn:de:0030-drops-76960
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7696/
Go to the corresponding LIPIcs Volume Portal

Ahrens, Benedikt ; Lumsdaine, Peter LeFanu ; Voevodsky, Vladimir

Categorical Structures for Type Theory in Univalent Foundations

pdf-format:
LIPIcs-CSL-2017-8.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{ahrens_et_al:LIPIcs:2017:7696,
  author =	{Benedikt Ahrens and Peter LeFanu Lumsdaine and Vladimir Voevodsky},
  title =	{{Categorical Structures for Type Theory in Univalent Foundations}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{8:1--8:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Valentin Goranko and Mads Dam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7696},
  URN =		{urn:nbn:de:0030-drops-76960},
  doi =		{10.4230/LIPIcs.CSL.2017.8},
  annote =	{Keywords: Categorical Semantics, Type Theory, Univalence Axiom}
}

Keywords: Categorical Semantics, Type Theory, Univalence Axiom
Collection: 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Issue Date: 2017
Date of publication: 16.08.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI