Re: [HoTT] Re: Precategories, Categories and Univalent categories

[Michael Shulman <shulman@sandiego.edu>]

It may be "indexed" in the sense that it involves maps into a
universe, but it is not an "indexed category" as the term is usually
used, since the latter is a pseudofunctor into Cat rather than a lax
functor into Span.  In particular, a displayed category can be a
fibration, an opfibration, both, or neither, while an indexed category
always corresponds to at least a fibration.  A displayed category is a
refinement of a functor in the same way that a dependent type is a
refinement of a function: you can always recover the total category by
taking Sigma-types, and thereby formulate all of the theorems
mentioned in your MR review.  The advantage of "presenting" a functor
as a displayed category is that it solves precisely the problem at
issue, giving a way of talking about two objects being "in the same
(strict) fiber" without invoking equality of objects in the base
category.

Requiring the type of objects of a category to be an h-set does also
recover the ability to talk about strict fibers, but the resulting
theory of "Grothendieck fibrations" would be pretty useless for HoTT,
since almost no naturally-occurring categories have this property or
can even be replaced by equivalent categories that have this property.
If we want a theory of categories that includes important things like
the category of sets, and toposes and geometric morphisms constructed
from it, we cannot require all categories to have h-sets of objects
(i.e. to be "strict categories").  Thus, to talk about fibrations, we
have to either use something like displayed categories, or a weaker
notion of fibration such as mentioned by Emily (in which case one
simply talks about "essential fibers" rather than strict fibers, and
these do have reindexing functors and all the other behavior one would
expect).

On Thu, Nov 8, 2018 at 1:08 PM Thomas Streicher
<streicher@mathematik.tu-darmstadt.de> wrote:
>
> > Actually, you don't need strict equality on categories to talk about
> > strict Grothendieck fibrations in type theory:
> > https://ncatlab.org/nlab/show/displayed+category
>
> This is indexed and not fibered (see my MR review of this paper).
>
> 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.