nLab
universe - contents

universe

(in category theory/type theory/computer science)

of all homotopy types

• type of types, object classifier,

  • univalence

• codomain fibration

of homotopy n-types

• type of n-types

of 0-truncated types/h-sets

• type of h-sets, universe in a topos

of (-1)-truncated types/h-propositions

• type of propositions, subobject classifier

resizing

• universe enlargement