Re: [HoTT] Precategories, Categories and Univalent categories

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

Dear Emily,

thanks for the various references. I was aware of Street's
generalization which is obtained from Grothendieck fibrations by
closing up under categorical equivalences.

But when one works with fibrations P : XX -> BB then it is intrinsic to
have have reindexing functors u^* : P(I) -> P(J) for all u : J -> I in
the base. And these one doesn't have in case of Street fibrations.

For me Grothendieck fibrations are a most useful tool for

1) categorical logic
2) category theory over toposes or even more general base categories
3) conceptual understanding of geometric morphisms and properties of them

and there the stronger notion of Grothendieck is indispensible.

For Street fibrations fibers over isomorphic objects need not be
equivalent anymore. That appears to me as counter intuitive. But,
well, speaking about fibers is evil anyway.

Thomas

PS  (1) Admittedly, in HoTT one needs fibrations less since one has
universes available. If I had to defense the HoTT view I would say
that fibrations are meaningless and they were used by the old category
theorists only because they lacked universes.

(2) In ordinary category theory, at least in topos theory, speaking about
internal categories is very important. I guess that is an eval notion
because it is built on equality of objects. Is there something like an
"internal quasicat"?


-- 
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.