Name
Abstract | ||
|---|---|---|
We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1109/LICS.2017.8005130 | 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
Keywords | DocType | Volume |
stack semantics,dependent type theory model,univalent universe,propositional truncation | Conference | abs/1701.02571 |
ISSN | ISBN | Citations |
1043-6871 | 978-1-5090-3019-4 | 4 |
PageRank | References | Authors |
0.57 | 7 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| T. Coquand | 1 | 135 | 13.55 |
| Bassel Mannaa | 2 | 19 | 3.49 |
| Fabian Ruch | 3 | 4 | 0.57 |