Showing changes from revision #0 to #1:
Added | Removed | Changed
Mike Shulman’s dependently typed first-order theory SEAR.
A model of SEAR is a dagger 2-poset with a set of elements in for every object such that
Nontriviality: There exists an object with a term , where is the propositional truncation of the type .
Relational comprehension: for every object and there is a function
Function evaluation: For every map , there is a function such that is contractible.
Tabulations: for every object and and morphism , there is an object and maps , , such that and for two 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 element , is contractible and (2) for every element , if there exists an object such that is contractible, then is in the image of .