Re: Composition of Fibrations and Quantification

[Richard Garner <richardgarner@fastmail.fm>]

Dear Neil, Steve,

Steve: what you say about fibrations and opfibrations is completely
correct. So if E ---> D is a bifibration, and D ---> C is a bifibration,
then the composite E ---> C is a bifibration. It is moreover easy to
check that if the individual parts of this satisfy Beck-Chevalley, then
so too will the composite. Thus the composite of fibrations with sums is
again a fibration with sums.

For products, though, I think the situation is a bit more complex. I
could not see how to derive the result by a simple duality. From
scribbling on the back of an envelope, it does appear to be true that:

- if E -p--> D and D ---q---> C are fibrations with products, then so
too is E ---qp---> C

The argument I have is basically the following. Given e in E with pe = d
and qd = c, and some f: c ---> c' in C, we wish to describe the Pi of e
along f; we'll write this as f_*(e). Well first we form f_*(d) in D, its
pullback g : f^*f_*(d) ----> f_*(d) along f, and the counit k: f^*f_*(d)
---> d in the fibre over c. Using these data in D,  we now form in E the
pullback k^*(e) of e along k and then the Pi along g, so yielding e' =
g_*k^*(e). Now pe' = f_*(d) and q(f_*(d)) = c' and it's now not so hard
to check that e' is in fact the Pi of e along f, as desired.

For the checking in the last step, I seemed to need a few times the
Beck-Chevalley condition for products. So I doubt one could get away
without that. I have not tried to verify whether the Pi's of the
composite so defined themselves satisfy the Beck-Chevalley condition,
but I would be amazed if this were not the case.

Finally, one might ask the following question. Suppose that E ----> D
and D ----> C are fibrations with products and sums, and that in each
case the sums and products satisfy the distributivity axiom
("type-theoretic axiom of choice"). Does the composite fibration, which
by the above again has sums and products, also satisfy the
distributivity axiom? I do not know the answer to this, but I rather
suspect so. It would be a largeish diagram chase. It would be nice to
know if there was a more abstract reason why this is true.

Richard


On Sun, Jun 8, 2014, at 11:58 PM, Steve Vickers wrote:
> Some thoughts:
> 
> * The result about composition of fibrations holds in any 2-category with
> comma objects and 2-pullbacks, not just Cat. (Think of the Chevalley
> criterion  for fibrations.)
> 
> * By duality on 2-cells it thus also applies to opfibrations, and hence
> to bifibrations.
> 
> * It is bifibration structure that gives you the left adjoints you ask
> for.
> 
> * For the right adjoints, look at the dual 2-category, where your
> fibrations  become bifibrations.
> 
> Hence it seems to me that your conjectures are all true, and even
> generalize  widely.
> 
> Steve.
> 
>> On 6 Jun 2014, at 10:47, Neil Ghani <neil.ghani@strath.ac.uk> wrote:
>> 
>> Dear All
>> 
>> We know that if p and q are fibrations, then their composition p.q is a  fibration.
>> 
>> But what about quantification … that is if reindexing along every morphism has a right/left adjoint in p and q, then does reindexing along  every morphism in p.q have a right/left adjoint? Under some circumstances?
>> 
>> Thanks for any thoughts
>> Neil

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]