Category theory
===============

Topos logic versus HoTT
-----------------------

.. 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.