Benedikt Ahrens ; Peter LeFanu Lumsdaine ; Vladimir Voevodsky - Categorical structures for type theory in univalent foundations

lmcs:4801 - Logical Methods in Computer Science, September 11, 2018, Volume 14, Issue 3 - https://doi.org/10.23638/LMCS-14(3:18)2018
Categorical structures for type theory in univalent foundationsArticle

Authors: Benedikt Ahrens ; Peter LeFanu Lumsdaine ; Vladimir Voevodsky

    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 univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps between the various types of structures, and show that assuming the Univalence axiom, some of the comparisons are equivalences. 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.


    Volume: Volume 14, Issue 3
    Published on: September 11, 2018
    Accepted on: September 4, 2018
    Submitted on: September 4, 2018
    Keywords: Mathematics - Logic,Computer Science - Logic in Computer Science,Mathematics - Category Theory,18C50, 03B15, 03B70,F.3.2,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Coq for Homotopy Type Theory; Funder: European Commission; Code: 637339
    • Research in Mathematics; Funder: National Science Foundation; Code: 1128155

    1 Document citing this article

    Consultation statistics

    This page has been seen 1571 times.
    This article's PDF has been downloaded 688 times.