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
Parametricity, automorphisms of the universe, and excluded middle
University of Birmingham.
University of Birmingham.
Stockholm University, Faculty of Science, Department of Mathematics. (Logik)ORCID iD: 0000-0003-1390-2970
University of San Diego.
(English)Manuscript (preprint) (Other academic)
Abstract [en]

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 in some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.

National Category
Algebra and Logic
Research subject
Mathematical Logic
Identifiers
URN: urn:nbn:se:su:diva-140146OAI: oai:DiVA.org:su-140146DiVA, id: diva2:1077739
Note

Submitted

Available from: 2017-02-28 Created: 2017-02-28 Last updated: 2022-02-28

Open Access in DiVA

No full text in DiVA

Other links

arXiv

Authority records

Lumsdaine, Peter LeFanu

Search in DiVA

By author/editor
Lumsdaine, Peter LeFanu
By organisation
Department of Mathematics
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 120 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