Dear Thomas, Thank you for your reply. Michael Warren also pointed out to me (in a private reply) that one can construct dependent products for split fibrations of internal groupoids. Unfortunately, this doesn't quite answer my question. As far as I know, Joyal--Tierney fibrations are cloven (or rather, cleavable), but they do not have to split. After all, in the case where the Grothendieck topos we start with is Set, the Joyal--Tierney model structure coincides with the standard model structure on Grpd, in which the fibrations really are just isofibrations in the usual sense. (I assume the axiom of choice here; the theory of cofibrantly generated model categories breaks down otherwise.) Incidentally, since you bring up universes, perhaps I should explain why I am focusing on Joyal--Tierney fibrations: I am wondering about the strength of propositional resizing. As you say, the groupoid interpretation makes sense constructively; but it is not hard to see that propositional resizing in the groupoid interpretation implies a weak form of the axiom of choice (namely, WISC) in the ambient set theory. This essentially boils down to the difference between weak equivalences (= fully faithful and essentially surjective on objects) and equivalences. The difference disappears when one restricts to Joyal--Tierney fibrations: this is a special case of the so-called "Whitehead theorem" in model category theory. -- Zhen Lin [For admin and other information see: http://www.mta.ca/~cat-dist/ ]