Stack Semantics of Type Theory
classification
💻 cs.LO
keywords
typetheorydependentmodelpropositionalstacktruncationunivalent
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.