Stack Semantics of Type Theory
Logic in Computer Science
2017-04-21 v2
Abstract
We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalising 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.
Keywords
Cite
@article{arxiv.1701.02571,
title = {Stack Semantics of Type Theory},
author = {Thierry Coquand and Bassel Mannaa and Fabian Ruch},
journal= {arXiv preprint arXiv:1701.02571},
year = {2017}
}