Stack semantics of type theory
- Thierry Coquand,
- Bassel Mannaa,
- Fabian Ruch
- University of Gothenburg,
Research Output:
Journal Article or Conference Article in Journal
Conference article
Peer-review
Open access
Publication Information
Output type
Research Output:
Journal Article or Conference Article in Journal
Conference article
Peer-reviewOriginal language
EnglishJournal (Volume, Issue Number)
Annual Symposium on Logic in Computer SciencePublication milestones
- Published - 23/06/2017
Publication status
Published - 23/06/2017
ISSN
1043-6871Publication IDs
- Scopus: 85034044408
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.
Publication metrics
PlumX, opens in new tab
Captures
20
Citations
19
Access to documents
Accepted author manuscript, 398.7 KB
License:Unspecified
Related Event
Title
Annual ACM/IEEE Symposium on Logic in Computer Science
Event type
ConferenceDegree of recognition
International eventDate
20/06/2017 - 23/08/2017Location
ReykjavikIceland