Showing changes from revision #2 to #3:
Added | Removed | Changed
A model of the Elementary Theory of Rel (ETRel) is the dagger 2-poset whose category of maps is a model of ETCS?.
A model of ETRel is a dagger 2-poset such that:
Always true relation: for every object and , there is a morphism such that for every other morphism , ,
Singleton: there is an object such that , and for every object there is an onto dagger morphism .
Cartesian products: for every object and and morphism , there is an object and maps , , such that .
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 .
Function extensionality: for every object and and maps , and , implies .
Natural numbers: there is an object with maps and , such that for each object with maps and , there is a map such that and .
Choice: for every object and , every entire dagger epimorphism has a section.