A new preprint is available on arXiv

http://arxiv.org/abs/1701.02571

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