Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
CATEGORICAL STRUCTURES FOR TYPE THEORY IN UNIVALENT FOUNDATIONS
Stockholm University, Faculty of Science, Department of Mathematics.
Number of Authors: 32018 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 14, no 3, article id 18Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
2018. Vol. 14, no 3, article id 18
Keywords [en]
Categorical Semantics, Type Theory, Univalence Axiom
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:su:diva-162963DOI: 10.23638/LMCS-14(3:18)2018ISI: 000450660200006OAI: oai:DiVA.org:su-162963DiVA, id: diva2:1270059
Available from: 2018-12-12 Created: 2018-12-12 Last updated: 2018-12-12Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Search in DiVA

By author/editor
Lumsdaine, Peter Lefanu
By organisation
Department of Mathematics
In the same journal
Logical Methods in Computer Science
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 87 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf