On Small Types in Univalent Foundations
We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what can...
| Auteurs principaux: | , |
|---|---|
| Format: | Article |
| Langue: | English |
| Publié: |
Logical Methods in Computer Science e.V.
2023-05-01
|
| Collection: | Logical Methods in Computer Science |
| Sujets: | |
| Accès en ligne: | https://lmcs.episciences.org/8643/pdf |