Augmenting Steve Awodey's reply to M. Shulman I want to mention a further possibility which is more in the spirit of type / category theory, namely that of universes in toposes as described in my article with the same title (available under (www.mathematik.tu-darmstadt.de/~streicher/NOTES/UniTop.ps.gz). It is essentially a catgorical variant of Martin-Loef's notion of universe albeit an impredicative one. It was used a lot in categorical semantics of type theory (starting ~1985) but certainly part of the categorical folklore. The first written account I know of is Jean B'enabou's "Probl`emes dans le topos" from 1973. His main example that time was decidable K-finite objects in a topos with nno. A universe in a topos EE is a pullback stable class SS of morphism admitting a generic element in SS, i.e. a map E -> U in SS from which all other maps in SS can be obtained via pullback. Replacement is modelled by the requirement that SS be closed under composition. Of course, one usually requires more further closure properties (as in type theory). In the above mentioned paper I have shown that all Grothendieck and realizability toposes admit such universes (exploiting Grothendieck universes on the meta-level). As far as I can see universes serve well the purpose of replacement in mathematics, namely defining families of types by recursion. They achieve this goal in a more direct way than replacement does. The reason why they are presumably weaker than the setting Steve mentioned is that one needs a type-theoretic collection axiom (as in Joyal and Moerdijk's "Algebraic Set Theory") besides W-types for constructing set theoretic universes from type theoretic ones. I don't know why universes have hardly been considered in topos theory. (One notable exception being B'enabou's calibrations giving notions of size when considering locally small fibrations.) I think they are most useful and actually indispensible for doing category theory in the internal language of a topos. Algebraic Set Theory is an instance of universes, namely universes within categories modelling first order logic. Thomas