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.TYPES.2017.6
URN: urn:nbn:de:0030-drops-100546
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/10054/
Go to the corresponding LIPIcs Volume Portal

Orton, Ian ; Pitts, Andrew M.

Decomposing the Univalence Axiom

pdf-format:
LIPIcs-TYPES-2017-6.pdf (0.5 MB)

Abstract

This paper investigates Voevodsky's univalence axiom in intensional Martin-Löf type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, collected together from various published and unpublished sources; we then present a new decomposition of the univalence axiom into simpler axioms. We argue that these axioms are easier to verify in certain potential models of univalent type theory, particularly those models based on cubical sets. Finally we show how this decomposition is relevant to an open problem in type theory.

BibTeX - Entry

@InProceedings{orton_et_al:LIPIcs:2018:10054,
  author =	{Ian Orton and Andrew M. Pitts},
  title =	{{Decomposing the Univalence Axiom}},
  booktitle =	{23rd International Conference on Types for Proofs and  Programs (TYPES 2017)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{104},
  editor =	{Andreas Abel and Fredrik Nordvall Forsberg and Ambrus Kaposi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/10054},
  URN =		{urn:nbn:de:0030-drops-100546},
  doi =		{10.4230/LIPIcs.TYPES.2017.6},
  annote =	{Keywords: dependent type theory, homotopy type theory, univalent type theory, univalence, cubical type theory, cubical sets}
}

Keywords: dependent type theory, homotopy type theory, univalent type theory, univalence, cubical type theory, cubical sets
Collection: 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
Issue Date: 2018
Date of publication: 08.01.2019
Supplementary Material: https://doi.org/10.17863/CAM.25036 (Agda 2.5.4 source code)

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