Re: [HoTT] Precategories, Categories and Univalent categories

[Emily Riehl <eriehl@math.jhu.edu>]

There’s a (2-categorical) characterization of fibrations due to Ross Street that I like that works well in the (∞,1)-categorical context. In quasi-categories this captures the class of maps that Joyal/Lurie call “cartesian fibrations” but this definition can be used for other models of (∞,1)-categories as well.

A functor p : E —> B between (∞,1)-categories is a cartesian fibration if the corresponding functor p^2 : E^2 —> B/p admits a right adjoint right inverse (right adjoint whose counit is invertible). 

A functor p : E —> B between (∞,1)-categories is a discrete cartesian fibration (aka right fibration) if the corresponding functor p^2 : E^2 —> B/p is an equivalence.

Here E^2 is the (∞,1)-category of arrows in E (the cotensor with the walking arrow category 2) while B/p is a pullback of B^2 along p : E —> B in the codomain variable.

If p : E —> B is an isofibration (in models, this is the notion of fibration in the corresponding model category; eg the Joyal model structure for quasi-categories) then p^2 : E^2 —> B/p is also an isofibration and you can modify the right adjoint right inverse so that the right adjoint is a strict section and the counit is an identity. This can be technically convenient — the adjunction is now a fibered adjunction and can be pulled back more easily — but strict equality doesn’t feel necessary to me in this context.

Best,
Emily

—
Assistant Professor, Dept. of Mathematics
Johns Hopkins University
www.math.jhu.edu/~eriehl

> On Nov 8, 2018, at 6:58 AM, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:
> 
> 
> Thorsten asked why I prefer to have strict equality on categories.
> The answer is that one needs it in category theory typically when
> speaking about Grothendieck fibrations.
> And the latter is most useful in many contexts in particular when
> understanding geometric morphisms. This by the way also extends to
> Grothendieck fibrations in quasicategories as in Joyal and Lurie's
> accounts.
> 
> Thomas
> 
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.