-
Singleton: there is an object such that for every other morphism , , and for every object there is an onto dagger morphism .
-
Function extensionality: for every object and , maps and , and global element , implies .
-
Relational comprehension: for every object and , there is a function
-
Tabulations: for every object and and morphism , there is an object and maps , , such that and for two global elements and , and imply .
-
Power sets: for every object , there is an object and a morphism such that for each morphism , there exists a map such that .
-
Natural numbers: there is an object with maps and , such that for every object with maps and , there is a map such that and .
-
Collection: for every object and function , there exists an object with a map and a -indexed family of objects such that (1) for every global element , is contractible and (2) for every global element , if there exists an object such that is contractible, then is in the image of .