| Autor: |
Booij, Auke B., Escardó, Martín H., Lumsdaine, Peter LeFanu, Shulman, Michael |
| Jazyk: |
angličtina |
| Rok vydání: |
2018 |
| Předmět: |
|
| DOI: |
10.4230/lipics.types.2016.7 |
| Popis: |
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. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
