Re: are fibrations evil?

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

Dear Michael,

Street's notion of fibration is a weakening not a strengthening of
Grothendieck fibrations. For such a thing the key intuitions are lost as
far as I can see (even if I and J are isomorphic the fibre over I may be
inhabited whereas the fibre over J is inhabited). I doubt that category
theory over a base (topos) can be deloped this way. At least it would be
very cumbersome. Has the generalised notion of fibration been used for
something?

I agree with you that Kan fibrations in simplicial sets are an alternative
and certainly the right thing if one want's to get "weak". After all that's
what I suggested in 2006 in a talk in Uppsala.
I personally am interested in the possibility of having type theories where
equality coincides with being isomorphic or even weakly equivalent (as recently
suggested by Voevodsky).
But this is an extremal point of view which shouldn't be taken absolute since
otherwise important parts of category theory get lost.

I suspect that when doing fibered categories in a type theory validating
Voevodsky's equivalence axiom one comes up with something like Street's
generalisation of fibrations. But that doesn't mean that we arrive at something
easy to work with.

What Martin Hofmann and I thought when bringing up the idea was that use of
intensional Id-types amounts to imposing a brutal bureaucracy which FORCES
you to check all the coherence conditions often swept under the carpet.

I think when interpreting type theory in the topos SSet of simplicial sets
one can have both extensional Id-types and the intensional ones. In the first
case a family of types is simply a map of SSet, in the second case it is a
Kan fibration. Luckily both system of display maps are closed under \Sigma and
\Pi. Thus the intensional model sits within the extensional one. It is the
restriction to "kosher" types, i.e. Kan complexes.

Thomas





[For admin and other information see: http://www.mta.ca/~cat-dist/ ]