{"entities":{"Q1115435":{"pageid":1126184,"ns":120,"title":"Item:Q1115435","lastrevid":66773862,"modified":"2026-04-12T12:46:20Z","type":"item","id":"Q1115435","labels":{"en":{"language":"en","value":"Toposes and intuitionistic theories of types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4085642"}},"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":"Q1115435$9672E286-5060-4773-B87C-8C92103A7001","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"de3b77169c3b91cabfb0c80046a98c491a9fa6d5","datavalue":{"value":{"text":"Toposes and intuitionistic theories of types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1115435$06A7BC4E-6364-4C1D-8596-FB9C5A7BD91C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"471c27b739aa08b1eddcf633f3015b63bf36cb0c","datavalue":{"value":"0664.03040","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115435$BF222D42-4820-447A-B8CD-45B445657E6B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a1a329786cddeeb3eb764e1d3c0ae3dd45b5805e","datavalue":{"value":"10.1016/0022-4049(89)90111-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115435$7779CB9C-7434-490D-B69C-E169C4EED146","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"34a2791b3d9645796ba9cdff19dd05bcf40f0161","datavalue":{"value":{"entity-type":"item","numeric-id":168348,"id":"Q168348"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115435$5734040F-38CE-4A4E-975A-21821883AE31","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7211ad5ca16eb0d22cd0051fff3d0f3af254ceb6","datavalue":{"value":{"time":"+1989-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1115435$6561A202-AEE5-451E-B758-8D046C7E0274","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"483ffe1d755fa9ce4fa2b7b94ff94b54266ef7aa","datavalue":{"value":"It is by now well-known that intuitionistic (higher-order) type theories correspond to toposes, in the sense that every such theory is ``embodied'' in a topos, and every topos has a canonical theory of which it is (equivalent to) the embodiment. The aim of this paper is to introduce a notion of translation of theories which makes this correspondence into an equivalence of categories, when arbitrary left exact functors are taken as the morphisms between toposes. (Previous authors had considered a more ``rigid'' notion of translation corresponding to logical functors between toposes.) Indeed, the correspondence becomes an equivalence of 2-categories, since the authors also introduce ``comparisons'' of interpretations which correspond to natural transformations between left exact functors.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115435$7BEE0BF5-59F6-4C17-BDE3-25727E0BFA3C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"957970e11422fbdef7ba9db5e2b00bc9584e024a","datavalue":{"value":"03G30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115435$1D605085-E398-49A0-9267-ADAE875D482B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b28ec93edbc28cf51ca38efd24d859f9e51258c9","datavalue":{"value":"18B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115435$F91EF484-F746-44F3-BCD9-02789C9EE3F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115435$0A312FAA-B313-41BD-B0A3-35F2C17F231B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115435$F674B222-72F8-457B-9A16-CA44C4F89038","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1d5307c4dbaa77ce89b6bff287817ef9ffbdef1c","datavalue":{"value":"4085642","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115435$825D7561-A132-4DE4-8A34-D26E45C3391E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0c01883259e404fee2a5dce79ae616b75b133ae8","datavalue":{"value":"intuitionistic type theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115435$E3ABF97B-74E1-43EF-B646-1298BF8B6C03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6313254f4f788b15928122ec7af54745a44506da","datavalue":{"value":"translation of theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115435$90CBE9B3-A93C-48EB-A103-764D7E237270","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9fb46f306f75a822dc888de123e29b19123ed077","datavalue":{"value":"equivalence of 2- categories","type":"string"},"datatype":"string"},"type":"statement","id":"Q1115435$DCFE6106-37FE-4E9F-8A20-CD66874C5F5E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3d82f8b03f6c1b8914585488abbd4230aebee772","datavalue":{"value":{"entity-type":"item","numeric-id":1303459,"id":"Q1303459"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115435$B018AAA5-8890-41DF-B871-E93D3FBD3818","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"decf1d047f45269e853a1e03e7b7e8c433616b96","datavalue":{"value":{"entity-type":"item","numeric-id":1840650,"id":"Q1840650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115435$34F70045-B5EA-483B-AEDF-9DCEE4B73A71","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"9596d005c29801249c01b9d1288aea39b7db279d","datavalue":{"value":{"entity-type":"item","numeric-id":702196,"id":"Q702196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115435$4D5BF592-6F51-4E05-A3C0-BB93FF3EB8DD","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":"Q1115435$F8C66983-5EE7-41A1-A378-CC8CF3AB77C6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"71656fc21323ed8e70b8896febf4e1a714ffc20d","datavalue":{"value":"https://doi.org/10.1016/0022-4049(89)90111-4","type":"string"},"datatype":"url"},"type":"statement","id":"Q1115435$0828B7AA-DEB1-4F3F-999A-347775BDEFD2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f9b483b5452ba5b019931b94cdc8a0392de56b03","datavalue":{"value":"W2020970787","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1115435$2E501F91-40F2-46DD-B479-220A508A57E0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cb3fb1f5163c51d21987992526ad7f1b03bc113","datavalue":{"value":{"entity-type":"item","numeric-id":5625124,"id":"Q5625124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115435$B9DAC591-215E-4E48-8E33-8F747802199E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d82b227295c10b6c3c9289b01dc8016d6c611441","datavalue":{"value":{"entity-type":"item","numeric-id":3727946,"id":"Q3727946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115435$1D3294CC-67B1-43C3-9086-F99A550AEEB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f40bcaa8d311e4db512eab174f3dec9cd00f54c","datavalue":{"value":{"entity-type":"item","numeric-id":5537599,"id":"Q5537599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115435$6E1CB09D-4AAE-4400-8D09-2C26117EF0A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e32699cd0a7711c981c20a75aa6c7b5a6208cd68","datavalue":{"value":{"entity-type":"item","numeric-id":5579018,"id":"Q5579018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1115435$10E7D11B-42EC-4A5A-9630-FEBC7C737A35","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"edc9fa361fa3867f7717436ced2f985449798e05","datavalue":{"value":{"entity-type":"item","numeric-id":4295233,"id":"Q4295233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"955ac5a384997a3457780c305c9edd90bfd6e2cd","datavalue":{"value":{"amount":"+0.8062513470649719","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":"Q1115435$C313A5D8-BF29-4A19-B1C4-1EE748CFF741","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ed54709a6f673f644ce42b4811f4136a63885141","datavalue":{"value":{"entity-type":"item","numeric-id":3333040,"id":"Q3333040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b5daea65dc43badc32a4421db03ac0d7d8f7941","datavalue":{"value":{"amount":"+0.8045836687088013","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":"Q1115435$39DDC04B-E736-4620-A044-8B6F3F3D2EA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ea27bdfec2ba133868d47d02bd5dc4fb070c1fe","datavalue":{"value":{"entity-type":"item","numeric-id":5752573,"id":"Q5752573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b1cb96caf85e7599563fc7316c222848f7f8918b","datavalue":{"value":{"amount":"+0.7976090908050537","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":"Q1115435$C9114848-A780-4E05-A91D-0BDFD1876A0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ed29d9908d77cfe49d55c60c6557d2016fe3a0ae","datavalue":{"value":{"entity-type":"item","numeric-id":3371526,"id":"Q3371526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11658041b9926f99122c618a91c8c40920715f02","datavalue":{"value":{"amount":"+0.7950611710548401","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":"Q1115435$DD272851-16D8-4AC8-86CF-CA541897AB73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e85a78009421682de717ef71d83034f0657ea380","datavalue":{"value":{"entity-type":"item","numeric-id":3481704,"id":"Q3481704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b6ba830072377fe3240b4c61c004432d8cc2d6b8","datavalue":{"value":{"amount":"+0.7710750699043274","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":"Q1115435$FB99871D-CAD5-4363-A41A-FCCB88815F90","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Toposes and intuitionistic theories of types","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Toposes_and_intuitionistic_theories_of_types"}}}}}