Repository logo
 

Decomposing the Univalence Axiom

Published version
Peer-reviewed

Type

Conference Object

Change log

Authors

Pitts, AM 

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.

Description

Keywords

dependent type theory, homotopy type theory, univalent type theory, univalence, cubical type theory, cubical sets

Journal Title

LIPIcs : Leibniz International Proceedings in Informatics

Conference Name

23rd International Conference on Types for Proofs and Programs (TYPES 2017), Post-Proceedings Volume

Journal ISSN

1868-8969

Volume Title

104

Publisher

Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Sponsorship
EPSRC (1641673)
Relationships
Is supplemented by:
Is source of: