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

[Michael Shulman <shulman@sandiego.edu>]

Right, the *forward* direction requires either equality of objects or
using "essential fibers" instead of fibers.  That's what I meant by
saying a displayed category is a "refinement" of a functor: you can
make a functor from a displayed category, but the opposite direction
is harder.  That doesn't mean that you can't express composition of
functors in terms of displayed categories: it just means you can't (or
shouldn't) do it in the naive way by first making your displayed
categories into functors, composing them, and then going back to a
displayed category.  Instead you just have to "lift" functor
composition to displayed categories in the same way that we lift
function composition to Sigma-types.

Suppose D is a displayed category over C, with types of objects obD(x)
: Type and types of morphisms D(f) : D(x) -> D(y) -> Type for x:ob(C)
and f:hom_C(x,y).  Then we can form a total category Sigma(C)D whose
type of objects is Sigma(x:ob(C)) obD(x) and whose types of morphisms
are similar Sigma-types.  Now suppose we have a further displayed
category E over Sigma(C)D.  Then applying associativity of
Sigma-types, we can construct a displayed category Sigma(D)E over C,
with type of objects ob(Sigma(D)E)(x) = Sigma(y:obD(x))obE(x,y) and so
on, whose total category is equivalent (indeed, definitionally
isomorphic, if Sigma-types have definitional beta and eta) to
Sigma(Sigma(C)D)E such that its projection functor corresponds to the
composite of the two functors.
On Fri, Nov 9, 2018 at 3:56 AM Thomas Streicher
<streicher@mathematik.tu-darmstadt.de> wrote:
>
> Benedikt and Peter essentially employ an old result of Benabou saying that
> functors to BB correspond normalized lax functor from BB^op to Dist,
> the bicategory of distributors. But, obviously, the forward direction requires
> equality of objects.
> Accordingly, they can't express composition of functors in terms of
> the associated normalized lax functors.
>
> Even classically, going from fibrations to indexed categories involves
> choice. But going from functors to normalized lax functors just
> requires equality of objects.
>
> 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.