Category theory

Topos logic versus HoTT

Todo

• toposes as models for types of h-level 0
• impredicativity: universe of sets as a topos
• \(\Sigma\), \(\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 \(\infty\)-toposes.