Showing changes from revision #3 to #4:
Added | Removed | Changed
< SEAR
A general (non-concrete) categorical version of Mike Shulman’s dependently typed first-order theory SEAR.
Assuming excluded middle, a model of categorical SEAR is a dagger 2-poset such that:
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 .