{"entities":{"Q5957856":{"pageid":8134658,"ns":120,"title":"Item:Q5957856","lastrevid":47759368,"modified":"2026-01-02T15:09:41Z","type":"item","id":"Q5957856","labels":{"en":{"language":"en","value":"Type theories, toposes and constructive set theory: Predicative aspects of AST"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1719171"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$EC594F6D-3C73-451F-BAA1-E10270033F22","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"43560caaf272f1bb38f48481094e41df2e5377a4","datavalue":{"value":{"text":"Type theories, toposes and constructive set theory: Predicative aspects of AST","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5957856$BC06F003-EF02-4088-906D-41AA4A618FA5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"da0db55bae3584ea688f8e08c4f69bb7fb634014","datavalue":{"value":"0999.03061","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957856$6EC68876-AFED-4E0A-8677-70CAF270E1E2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7d553806f4d64701cb4790bd2714397ffae451ca","datavalue":{"value":"10.1016/S0168-0072(01)00079-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957856$2F9D2D92-FC6C-4BA4-A755-1EDCF93B74D7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5d27f35d8b8d36daa01c278530444ad70355c66c","datavalue":{"value":{"entity-type":"item","numeric-id":169786,"id":"Q169786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$4CFC22F9-F6E0-4DAE-9CC3-F521535D7F9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8b28a0624df5a1c85ecb5bea565385eff5d13458","datavalue":{"value":{"entity-type":"item","numeric-id":185810,"id":"Q185810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$409B8CED-F680-4D0A-BBD6-A3C1A4C7E74B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$6F72332A-6550-4FA9-BC06-DD1FE514E3E3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4d77b9ad71b27c8447698ef69ee23e23f623e26d","datavalue":{"value":{"time":"+2002-12-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5957856$240A3D17-BCCE-402B-BE37-CAFFF88EA959","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"424fc7c4baf7a57b388dd582a24b16be9c15e90f","datavalue":{"value":"The correlation between type theories and categorical structures (e.g., simply-typed lambda calculus and Cartesian closed categories) is very significant in categorical logic. The categorical counterpart of higher-order intuitionistic logic is topos theory, which is essentially impredicative in nature. The authors present a categorical counterpart of constructive predicative type theories, such as Martin-L\u00f6f's, which is called a ``stratified pseudotopos''. They show that the sheaves on an internal site in a stratified pseudotopos again form such a pseudotopos. They also show that any stratified pseudotopos provides a model of Acz\u00e9l-Myhill set theory.","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957856$87DA7B14-5038-4B2F-ADFF-14D249378CD4","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"50a4d88aaef452ee91d36bc895e7495d5ed6f713","datavalue":{"value":{"entity-type":"item","numeric-id":195143,"id":"Q195143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$C7129380-5558-4039-8E31-1888945625D4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"957970e11422fbdef7ba9db5e2b00bc9584e024a","datavalue":{"value":"03G30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957856$EE676F15-DD59-4D0C-AB62-2322C775AF0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957856$0ED4EB24-B105-48FE-931D-5E27F5C031B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b28ec93edbc28cf51ca38efd24d859f9e51258c9","datavalue":{"value":"18B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957856$B60B5DEF-0425-41E5-AE28-172BE52F2907","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b0919c48a255b26fcf065230a9a621cd8c579a3","datavalue":{"value":"03E70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957856$34B474C6-67E5-4E17-B478-DA20F61E326E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957856$7BAFC8D2-5297-4FC7-9B0B-CE9E3C5E3F2E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"50f6c9576b735f04e50f703febe45e4400fb7796","datavalue":{"value":"1719171","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957856$B4582318-F6B2-405E-A70B-EB11EEBDA45A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6c658f92cfca10399e0b9df9aa408c3bc22cae6","datavalue":{"value":"constructive type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957856$15042D60-9305-4502-96EF-E3BD9FB0B1C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"60eebb1e4aa77101496dfa4fb7b74612facb8c11","datavalue":{"value":"predicative type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957856$5A3CA413-E292-4B0A-8DC1-F05D2CE6CC3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8902e506e56978ced118587e65eb775a1247cea7","datavalue":{"value":"categorical logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957856$E367539B-A106-4631-8FF0-755A57978807","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b45978cc1f07424b684d69690e94e969bb5cd8ab","datavalue":{"value":"topos theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957856$D6C224AD-97F5-4B83-885A-A4EB0F4378C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9ee054c8c42d187b49f517e71febcbe6c612fa4d","datavalue":{"value":"sheaves","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957856$7CF6355C-0241-4AF7-9F63-51EA52392B9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"282f5e0b34ced7750e5f9055ee020032a321d02f","datavalue":{"value":"stratified pseudotopos","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957856$43217AD0-2CB6-4BA1-BE6C-AF84A34A4E85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"450ff3b5c42a8a279c7f18055903a35b5ff65074","datavalue":{"value":"Acz\u00e9l-Myhill set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957856$2AB8666A-F411-4961-9147-422D6A2D97BB","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$BE7ADD28-D265-4BFA-BF00-F2B53D136FC2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e21df1d3055daa4725f01a29fad1e4853704fa4c","datavalue":{"value":{"entity-type":"item","numeric-id":3762311,"id":"Q3762311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$32D4B05E-5825-483D-8D5C-D77A71074363","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a560a6ffb5c4d05293e32c5701628ac370d7722a","datavalue":{"value":{"entity-type":"item","numeric-id":3869509,"id":"Q3869509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$591942C6-27A0-4C89-A2E7-95F720AD37F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb2c0b5e8230f2871b84c948850a6644a2216797","datavalue":{"value":{"entity-type":"item","numeric-id":1976877,"id":"Q1976877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$AC66F551-0546-4A36-8163-F354E09D1A6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"889c98b06b71353ead9711d9cef7ccbd6f932035","datavalue":{"value":{"entity-type":"item","numeric-id":3214890,"id":"Q3214890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$F2672BCF-404A-48CF-8DDA-D8B602E6A8EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0734eca8b44b27cc39aa495faea7cd858d51f4e1","datavalue":{"value":{"entity-type":"item","numeric-id":4247303,"id":"Q4247303"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$5A091B33-4AD4-42A9-BD56-054CA571735C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae56cbc30bf4e0ace39780e420d931108cdd0102","datavalue":{"value":{"entity-type":"item","numeric-id":4145861,"id":"Q4145861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$20470D95-11B1-4BA9-B814-9C9F3EAF3808","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2b4d0b84553ace3c1686bd305b88438b8dcb98e4","datavalue":{"value":{"entity-type":"item","numeric-id":4853985,"id":"Q4853985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$70F4B026-D36E-4DD5-83FE-A10890251039","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4da806e6297e618e7714c75d11216ab0dccef6a6","datavalue":{"value":{"entity-type":"item","numeric-id":1189567,"id":"Q1189567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$B63BAC23-1C79-4437-8596-0DE0F16A8F40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"72bce0021a20e6075192b92537623e64018b293b","datavalue":{"value":{"entity-type":"item","numeric-id":4099614,"id":"Q4099614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$6C7A9B66-FFE8-4AFF-A2E0-B8FB55A8D1F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$918222FA-71E3-4583-8509-B8C6C4639C77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75fbf88ad4b38bd2537051ad7d167bb814dd65eb","datavalue":{"value":{"entity-type":"item","numeric-id":1577483,"id":"Q1577483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$3BB538BB-2640-473B-815C-C263B7A19931","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74605135c388db78d4d0ca86dc0cd54881585bea","datavalue":{"value":{"entity-type":"item","numeric-id":4073362,"id":"Q4073362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$1D688B1A-5C98-48B7-B56E-7DFB471293A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a3f5182c5f84b08fd5162da8260189a7d667355c","datavalue":{"value":{"entity-type":"item","numeric-id":4247308,"id":"Q4247308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$334271CA-67B3-4166-894A-88372B8B2E2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"385f9359a1dec0777500656b0fbfb3f247ade24a","datavalue":{"value":{"entity-type":"item","numeric-id":3313859,"id":"Q3313859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$F269B6E9-1DA6-459B-A251-F00CF0353A17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2002e9228b023d08f49489031907fa50fb1b3491","datavalue":{"value":{"entity-type":"item","numeric-id":1188500,"id":"Q1188500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$2040BB64-A5C3-4533-9220-FC5CB7167AB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"273ec91c41490e9f7324cfe300f5c297eddfee74","datavalue":{"value":{"entity-type":"item","numeric-id":4175559,"id":"Q4175559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957856$41AF1273-9A25-4594-A75C-0B7846AEDECA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6b5baf50c06c5e66c9d629322d05e830dd879c9d","datavalue":{"value":"https://doi.org/10.1016/s0168-0072(01)00079-3","type":"string"},"datatype":"url"},"type":"statement","id":"Q5957856$48F73572-0BA5-41BE-9E82-362639411B9C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e7991d1c586eb2b12c4be9dc7a1098b5affbcd12","datavalue":{"value":"W2121213425","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957856$A1A70759-3778-45BC-A3B5-CAD37413B097","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"05bfee325e91f298337d8811e53f0e47fcab7290","datavalue":{"value":{"entity-type":"item","numeric-id":958492,"id":"Q958492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2727194c0bedddfe1a7965d2a10c35c14a2bbfd3","datavalue":{"value":{"amount":"+0.7737163305282593","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5957856$978A27B5-4C9D-435C-8A9D-09D05A8DA142","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b811cf4c0cb2dac863c6cb610bcaac1301e3ea3","datavalue":{"value":{"entity-type":"item","numeric-id":5718562,"id":"Q5718562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"58dfc75fdb1e7c020122024b2a4ed092082743ba","datavalue":{"value":{"amount":"+0.7717002630233765","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5957856$889D997A-F1E8-422E-8845-D6D44DB58BE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b04e63430efaf483a34bc67baaa14b820a6a99ae","datavalue":{"value":{"entity-type":"item","numeric-id":4680361,"id":"Q4680361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36b1cb62201bf64123dfcebcef762cd88adb08f7","datavalue":{"value":{"amount":"+0.7711936831474304","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5957856$C2AB043A-FEAC-451A-B0C2-118A946282F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b229fdf3be6e29888a59c1cd99bc0786aab224e","datavalue":{"value":{"entity-type":"item","numeric-id":556819,"id":"Q556819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d471d1a39d2a6c66abd8bd3bac757d88b9b721c","datavalue":{"value":{"amount":"+0.7549876570701599","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5957856$1865843E-E006-4DF3-9357-D0AF1BBC4A50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d0bb54b562fc2c6e0f3fe2cc79c360c6a28e307d","datavalue":{"value":{"entity-type":"item","numeric-id":448336,"id":"Q448336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81c84952f2c15e5710b39c1bbfaa1c4041948228","datavalue":{"value":{"amount":"+0.7542931437492371","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5957856$E0CC74F1-C2F9-4C4A-B172-A2198058495A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5957856","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5957856"}}}}}