.. todo:: - toposes as models for types of h-level 0 - impredicativity: universe of sets as a topos - :math:`\Sigma`, :math:`\Pi` and prop trunc already in toposes
.. todo:: a 1-topos or PW-pretopos may arise as the truncation of various *different* higher toposes
.. todo:: refer to ahrens et al approach to univalent categories etc
.. todo:: maybe you should split this up doing cat thy internally, and cat theory in general, in particular :math:`\infty`-toposes.