A new preprint is available on arXiv
where we present a stack semantics of type theory, and use it to
show that countable choice is not provable in dependent type theory
with one univalent universe and propositional truncation.
Bassel, Fabian and Thierry