Re: Fibrewise opposite fibration

[Martin Bidlingmaier <martin.bidlingmaier@mbid.me>]

[-- Attachment #1: Type: text/plain, Size: 4112 bytes --]

2-monad theory and related model categories of sketches could be relevant here, because these techniques reduce the problematic case of a non-split fibrations F that was raised by David in his initial message to the easy case of an equivalent but split fibration F’. In terms of logical foundations, this requires sufficiently large universes, but I expect (but haven’t verified) that you can do without choice.

I’m not sure I remember all the details correctly, but let me try to outline how this should work. Consider the category of sketches for fibrations: A sketch for a fibration is given by a functor E -> B and for each morphism f in B a set of “cartesian-marked” morphisms M_f in E that map to f. Morphism of sketches are commuting squares of functors that preserve Cartesian markings. Note that Cartesian-marked morphisms need not actually be Cartesian. Every fibration has a natural strucuture as sketch, where precisely the Cartesian morphisms are Cartesian-marked. And every sketch generates a fibration with natural marking. Informally, this generated fibration is obtained by freely adding morphisms to E so that all the M_f are non-empty and then adding commutative diagrams so that every Cartesian-marked morphism is actually Cartesian. Finally, one closes M_f under isomorphism over E.

More formally, there is a model category structure on sketches such that precisely the naturally marked fibrations are fibrant objects, and the equivalences of fibrant objects are the componentwise equivalences in the arrow category on Cat. Fibrant replacement of a sketch is given by the informal free generation I explained in the previous paragraph. (Note that there’s a naming collision here: Fibrations in the sense of Grothendieck fibrations and in the model categorical sense.)

Now, if you use Garner’s small object argument you get a fibrant replacement functor. Crucially, this fibrant replacement functor is the monad you get from a 1-categorical adjunction with the category of “strict” Grothendieck fibrations. These are given by Grothendieck fibrations with a cleavage, and their morphisms are commuting squares of functors that preserve cleavage on the nose.

Why does this give you the equivalent split fibration F’ from a non-split fibration F I promised in the beginning? Like so: You first map F (considered as a naturally marked sketch) into the category of strict (in particular: split) fibrations via the left adjoint I mentioned in the preceding paragraph. From there you apply the right adjoint to get back to sketches, which is simply given by forgetting the cleavage and taking the natural marking to obtain F’. F -> F’ is an equivalence, and F’ has a cleavage by construction.

If you want to know more about this you might want to take a look at my paper on models of type theory in lcc categories and its citations: https://protect-au.mimecast.com/s/J0ogCoV1Y2SzmkQri1YV08?domain=arxiv.org
Among other things, this paper defines the model categories of sketches for lcc categories and strict lcc categories. Grothendieck fibrations should work entirely analogously. I believe Lack’s “Homotopy theoretic aspects of 2-category theory” works out the “strict” model category of strict Grothendieck fibrations I mentioned above in the generality of an arbitrary 2-monad, but I’m not aware of a general model categorical treatment of sketches.

On Wed, Jan 31, 2024 at 17:41, <[streicher@mathematik.tu-darmstadt.de](mailto:On Wed, Jan 31, 2024 at 17:41,  <<a href=)> wrote:

> If we work with split fibrations and arbitrary cartesian functors between
> them we can construct the opposite of a fibration without quotienting.
> That is possible but in my eyes less elegant than the usual approach where
> one assumes that one can factorize modulo equivalence relations even if
> they are big.
>
> Thomas
>
> ----------
>
> You're receiving this message because you're a member of the Categories mailing list group from Macquarie University.
>
> Leave group:
> https://protect-au.mimecast.com/s/H5fJCp81gYC8Z57nfDKrk8?domain=outlook.office365.com

[-- Attachment #2: Type: text/html, Size: 8525 bytes --]