The Coq mailing list

[Thomas Streicher <streicher AT mathematik.tu-darmstadt.de>]

Dear Carlos,

the presheaf topos of simplicial sets certainly hosts a model of at
least intuitionistic set theory (IZF) as follows from the work on
algebraic set theory (AST). However, the homotopy interpretation of type
theory in sSet is not of this kind. So the AST technology is not
immediately applicable her.
Actually, even in extensional Extended Calculus of Constructions (ECC) 
even in presence extensionality for Prop (equivalent propositions are
equal) it is not known whether one can construct a model of IZF, say.
What's lacking is a (as I call type theoretic) "Collection Axiom"
typical for AST. More discussion of this problem you find in the
second paragraph of 

   www.mathematik.tu-darmstadt.de/~streicher/NOTES/UniTop.ps.gz

on p.8.
In other words I don't know the answer to your question and I haven't
heard of any successful attempt to solve it.

Thomas