Are Joyal--Tierney fibrations exponentiable?
Dear categorists, Consider the category M of internal groupoids in a Grothendieck topos, equipped with the Joyal--Tierney model structure where the cofibrations are the injective-on-objects functors and the weak equivalences are the fully faithful functors that are essentially surjective on objects (the latter in the sense of internal logic). Are the fibrations in this model structure exponentiable in the sense that pulling back fibrations along a fibration has a right adjoint? Notice that M is a right proper model category in which the class of cofibrations is closed under pullback, so if the answer to the above question is yes, then the Lumsdaine--Warren construction can be applied to obtain a model of dependent type theory with identity types, dependent products, dependent sums, coproducts, etc. Best wishes, -- Zhen Lin [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
The groupoid model of Martin Hofmann and me does make sense in any topos with say NNO. For getting universes you need universes in the topos. But this is about getting split models. But I'd expect everything goes through also for non-split models. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (2)
-
Thomas Streicher -
Zhen Lin Low