Are Joyal--Tierney fibrations exponentiable?

Are Joyal--Tierney fibrations exponentiable?

[Zhen Lin Low]

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/ ]

Re: Are Joyal--Tierney fibrations exponentiable?

[Thomas Streicher]

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/ ]

Re: Are Joyal--Tierney fibrations exponentiable?

[Zhen Lin Low]

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/ ]