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/ ]