10.1 The category of sets

Recall that in cha:category-theory we defined the category $𝒮et$ to consist of all $0$-types (in some universe $𝒰$) and maps between them, and observed that it is a category (not just a precategory).We consider successively the levels of structure which $𝒮et$ possesses.