Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
While I didn’t write this:
The point is that morphisms are regarded as stand-ins for (the families of) their fibers: In saying that such a morphism “is $U$-small” one means to say that all its fibers are $U$-small, hence that it represents a family of $U$-small sets.
Here the index-set of these $U$-small sets itself need not be $U$-small. In this sense every identity morphism counts as being $U$-small, since it represents a family of singleton sets.
Finally, the notation “$el$” is meant to refer to the “elements” of the universe, I think.
(All of this would be good to further clarify in the entry. But I won’t edit at the moment.)
Sure, if you have a reference that is useful to you, then it is probably useful to others, too, and worth adding.
And yes, the idea of universes and of object classifiers is a generalization of that of subobject classifiers: the latter are universes of (just) (-1)-truncated objects.
This is a rather general theme that is touched on in many entries, but I am not sure if we have one that serves as a stand-alone introduction for readers completely new to the perspective.
The entry relative point of view could have been such an entry point, but it remains a stub.
The entry categorical models of dependent type theory, which is all about this theme, too, is more extensive, but it hardly serves as an introduction.
1 to 6 of 6