{"entities":{"Q1024547":{"pageid":1026395,"ns":120,"title":"Item:Q1024547","lastrevid":66568119,"modified":"2026-04-12T10:59:58Z","type":"item","id":"Q1024547","labels":{"en":{"language":"en","value":"On the strength of dependent products in the type theory of Martin-L\u00f6f"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5565755"}},"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":"Q1024547$8F44BB16-5867-4575-BBA3-C13B24D14E79","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ddd54264b04c9cc88d45e24923a663f05a78e011","datavalue":{"value":{"text":"On the strength of dependent products in the type theory of Martin-L\u00f6f","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1024547$69822958-E6DE-49F2-A17D-497D74759CF9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c3fda305ea8c8cbd64cda2db24e38a7fa50d936a","datavalue":{"value":"1171.03004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024547$572516DF-9B04-4580-A2D8-7F0E49F13D18","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"db41a60b03ac22c1792510784e84140716e00bef","datavalue":{"value":{"entity-type":"item","numeric-id":323665,"id":"Q323665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024547$790D534F-BB4F-457B-8898-23D419D4352F","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":"Q1024547$4E76DE74-1839-40DC-89FD-9471E58EB3FC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b56d9fd9827ead92e1d841b592f7852bcfece777","datavalue":{"value":{"time":"+2009-06-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1024547$B74CBE7E-B3C5-419E-B18E-698F15CFE93E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6fd1ff6e6fd119807aa99e30c215d11ea76047b8","datavalue":{"value":"https://arxiv.org/abs/0803.4466","type":"string"},"datatype":"url"},"type":"statement","id":"Q1024547$6FCC3F33-B490-418E-A5B5-F354DAF8C6CB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024547$19ACFD4A-6768-4AA8-941D-C981FF1A5BE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3068729a394ad5bf58a1a3e5b5d24254d962e1a7","datavalue":{"value":"03F55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024547$8D4A3AC6-40AD-4E75-9491-73B782B333BD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"68a17f94d673ea46763ced78520d80d304222c91","datavalue":{"value":"5565755","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024547$E8DBDA25-D986-4C39-84F9-33BAB4FD22CF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13fd823fa813aa32375d6c4605d9195c2318674c","datavalue":{"value":"dependent type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024547$C919C510-EABF-4AF8-85E1-B9BB3E8C6A00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b1ec0f2e5cceb30f30511f344d3b5667cb913313","datavalue":{"value":"dependent products","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024547$DBDAD2A2-55D6-48AC-9E6D-874B46804B69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d8aa514cce6078d9005224c723c2e91bf199efa0","datavalue":{"value":"function extensionality","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024547$80B32DFE-86D0-44B2-AF9B-50CF446D9266","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"454090389315247a59dda8a7c520ea2795715012","datavalue":{"value":"Martin-L\u00f6f type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024547$2EDED802-DE80-4875-A39A-DEADCB689602","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"26ed17f0fa3b284d6eda2a0b6f59f94f851c6b48","datavalue":{"value":"elimination rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q1024547$5638A074-F4BB-407E-BB9E-0A79CF1CB0EE","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":"Q1024547$DC43B805-0640-4017-8DE8-04F806A559BE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"17f8b92f73498913bca700b31f0428e22d6c6f2d","datavalue":{"value":"W2151011698","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024547$4BAE641E-2B86-4C4B-8DD5-76C942E8C5E6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"49862011e061c40f77cd7e82e87d964c5d5edab7","datavalue":{"value":{"entity-type":"item","numeric-id":3395310,"id":"Q3395310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024547$34D4A28D-C82A-4BCB-BF35-9755D9C9F876","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d846dce50adc7b6741cb464e66a4207934b87faa","datavalue":{"value":{"entity-type":"item","numeric-id":4647577,"id":"Q4647577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024547$A375E1CB-C069-4D29-9967-0199C581BDCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48a73b0bc94774198cd192d06e32293454cda383","datavalue":{"value":{"entity-type":"item","numeric-id":4225149,"id":"Q4225149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024547$B206D520-BBCF-4A6D-A868-E81306CA31E1","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":"Q1024547$9E91A93F-7C0B-4377-8F54-9FF0FDB3AE5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d91a6fc5a255cbadfa617ce94146193166c4f9ed","datavalue":{"value":{"entity-type":"item","numeric-id":4247306,"id":"Q4247306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024547$0ADCD8B6-0CEA-481D-B9EB-A06AED496227","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ab5d7b35f67f940445411fa45c1b02bcb40d39f","datavalue":{"value":{"entity-type":"item","numeric-id":3999860,"id":"Q3999860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024547$AD5FC01F-30EC-4769-A18D-6D201CF27958","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"02e642d35b27f6202fe5a95f273070d49f953ce5","datavalue":{"value":{"entity-type":"item","numeric-id":3691668,"id":"Q3691668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024547$75AC7B21-1FE0-48C5-9565-E7C50EE8BEE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25fc0f83d5ec3109942a6da644b57709f31b1dc6","datavalue":{"value":{"entity-type":"item","numeric-id":1188522,"id":"Q1188522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1024547$7CE2DECF-4712-4713-B249-E690DEA2774E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"da78ee0d2d8926a57a253ae6eb4ba3ad644578b8","datavalue":{"value":"10.1016/J.APAL.2008.12.003","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1024547$5959A749-86D7-434B-91BB-6783F2BF51CD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"751cf0dec4b636680ca47b8e354d59854960ee3d","datavalue":{"value":{"entity-type":"item","numeric-id":688734,"id":"Q688734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44423c88c360dc13c65e26fef4451fd6a04fd8a6","datavalue":{"value":{"amount":"+0.89797807","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1024547$FC847BE0-021E-43B1-A461-F573FD4FB3F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f74c98b5a48e2ad52f2ae1ef2655d9c93c15c5d6","datavalue":{"value":{"entity-type":"item","numeric-id":3322097,"id":"Q3322097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"47f8eb0577cc9a0f6cb14e9793bce9d7a1b679b8","datavalue":{"value":{"amount":"+0.8966403","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1024547$2CF19EEB-7D0D-42E4-A0C2-6A72A6DD1685","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca5d922db37ef1718202e561077e8c4a52fe341f","datavalue":{"value":{"entity-type":"item","numeric-id":5492817,"id":"Q5492817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16c79ba1766079457871aa35b024242a01c768bc","datavalue":{"value":{"amount":"+0.89290214","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1024547$B5C812A4-AA77-4AB9-9E41-135340E2528C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"683c504ed0f54696319c3c2757e80c1a4f9b2a8b","datavalue":{"value":{"entity-type":"item","numeric-id":5879185,"id":"Q5879185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"210466822852efe0ebe038ca78e6495eacfa17c7","datavalue":{"value":{"amount":"+0.890782","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1024547$E17FF2AA-5EF3-4741-A500-7E28A06286ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"071577697c11a2c9b8cea4d5bf370cc8ab8c50a2","datavalue":{"value":{"entity-type":"item","numeric-id":4236885,"id":"Q4236885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0f6fff2d27264ce6e0a1884c39680a9c85f685ee","datavalue":{"value":{"amount":"+0.890477","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1024547$FBA56F22-D06E-4D6C-B82B-3970D67E9B73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39027ed63c2a2a68a2e6225028f9c1d4f4901f0f","datavalue":{"value":{"entity-type":"item","numeric-id":1099173,"id":"Q1099173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bf89f67683761ab64fbbf42ecea5821d1ffe12c9","datavalue":{"value":{"amount":"+0.88725674","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1024547$AAFAB10A-09C7-45CE-AF55-756FEB013CA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"26c0867e245a452e44f078e1a0c502914012c5dc","datavalue":{"value":{"entity-type":"item","numeric-id":1295372,"id":"Q1295372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8bf12333b0d5d001b5ba46a950e8529f66998d40","datavalue":{"value":{"amount":"+0.88484","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1024547$1587E00A-F6F4-4591-94C2-0B15940DAA1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d4fb6d6bfff67a2f1258b657ed2373278dedb60f","datavalue":{"value":{"entity-type":"item","numeric-id":5277981,"id":"Q5277981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"567180fdf27ff6c6fccd3ee465467301919fffc6","datavalue":{"value":{"amount":"+0.88400745","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1024547$09D69C66-5908-4E1E-B4C1-3C9BB56DEDFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc640084c58d56128b6c439ca219936b0844bd22","datavalue":{"value":{"entity-type":"item","numeric-id":3613313,"id":"Q3613313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ae72e9a6a13b5fb39365850b223f089bbb36415","datavalue":{"value":{"amount":"+0.88250935","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1024547$0AB470B9-AA52-4F15-B141-1CF975B9A907","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a86783be468d2adab8db2bcfe00a00cc438adddd","datavalue":{"value":{"entity-type":"item","numeric-id":813417,"id":"Q813417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ae72e9a6a13b5fb39365850b223f089bbb36415","datavalue":{"value":{"amount":"+0.88250935","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1024547$E83E93C9-25D1-40DB-87FF-3A874DF2A01B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On the strength of dependent products in the type theory of Martin-L\u00f6f","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_the_strength_of_dependent_products_in_the_type_theory_of_Martin-L%C3%B6f"}}}}}