Parametricity, automorphisms of the universe, and excluded middle

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

Colleges, School and Institutes

External organisations

  • Stockholm University
  • University of San Diego

Abstract

It is known that one can construct non-parametric functions by assuming classical
axioms. Our work is a converse to that: we prove classical axioms in dependent
type theory assuming specific instances of non-parametricity. We also address
the interaction between classical axioms and the existence of automorphisms of
a type universe. We work over intensional Martin-Löf dependent type theory,
and for some results assume further principles including function extensionality,
propositional extensionality, propositional truncation, and the univalence axiom.

Details

Original languageEnglish
Title of host publicationProceedings of 22nd International Conference on Types for Proofs and Programs, TYPES 2016
Publication statusE-pub ahead of print - 27 Jun 2017
Event22nd International Conference on Types for Proofs and Programs, TYPES 2016 - Novi Sad, Serbia
Duration: 23 May 201626 May 2016

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherDagstuhl Publishing
ISSN (Electronic)1868-8969

Conference

Conference22nd International Conference on Types for Proofs and Programs, TYPES 2016
CountrySerbia
CityNovi Sad
Period23/05/1626/05/16

Keywords

  • Relational parametricity, dependent type theory, univalent foundations, homotopy type theory, excluded middle, classical mathematics, constructive mathematics