{"entities":{"Q2881097":{"pageid":2891817,"ns":120,"title":"Item:Q2881097","lastrevid":58039698,"modified":"2026-04-03T13:48:29Z","type":"item","id":"Q2881097","labels":{"en":{"language":"en","value":"On irrelevance and algorithmic equality in predicative type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6021346"}},"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":"Q2881097$A1E9A6EC-9FD5-49E4-BD65-09EBC0E61281","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d3dc0d0c87cfab3e1b78424c8a743ecb6a81499a","datavalue":{"value":"1238.03028","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881097$D24B8B2F-C9D7-468B-8A1D-806485D6F95D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"82e9a1066a210b96380f3ba5200e0b3031f66217","datavalue":{"value":"10.2168/LMCS-8(1:29)2012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881097$36CB05A2-9A7C-43A5-8790-B3B91DABA8F0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9fd295c773add0c694cee3f65e8e7cf93dc4bc27","datavalue":{"value":{"entity-type":"item","numeric-id":923882,"id":"Q923882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881097$D2912D62-378F-4548-8D16-94DBF31FB51D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"22d4f40940ae63e936c21b3ba75f359788c389e1","datavalue":{"value":{"entity-type":"item","numeric-id":1652973,"id":"Q1652973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881097$15010CCF-D351-4D1F-818B-E7CA927C7603","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881097$154B2CDA-C918-4F3C-89B9-8CA21A17131B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d567b51f320d6b206f1e246178a080db047a3948","datavalue":{"value":{"time":"+2012-04-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":"Q2881097$CE3DD277-AB38-4548-A4AB-C729456B0C61","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2e50f24b9576cffbbcd8ce1b50c338755e894bd1","datavalue":{"value":"https://arxiv.org/abs/1203.4716","type":"string"},"datatype":"url"},"type":"statement","id":"Q2881097$7657D8DF-626E-49B4-8FB2-4DE23C9360EA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881097$F5AFB265-12A7-4F50-A847-B35A2E698922","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881097$92461DDB-9261-4FC1-B958-F47C0B145056","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bdc0c9defc03dccf8496685a4a894a539988fda8","datavalue":{"value":"6021346","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881097$717E014B-C2C8-407E-A3E1-8E76C9C34079","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881097$33867A41-573A-46B3-B1C7-C066E0AA481B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fda5d8057392e50193b0eca80d9562ae727873ec","datavalue":{"value":"proof irrelevance","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881097$D1176EEA-28E9-4D5E-A451-843E0B959346","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"284a21fa8c63aa0312b95a28504a08c1729085b4","datavalue":{"value":"typed algorithm equality","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881097$01154BB9-EF66-4969-92BA-82B04E5EF499","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fd09c797952a268ece59feabb30b339489339461","datavalue":{"value":"logical relation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881097$DC2A7F36-F732-4AFB-A42B-FC22F58D5C83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2a3c42e92edacb9578ee7aa6e6989b083d06b242","datavalue":{"value":"universal Kripke model","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881097$12F2AEF9-C301-4C9A-838E-6F6D34C26735","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e41927344b9397ba2eb05288d661d38c0f0d55a6","datavalue":{"value":{"entity-type":"item","numeric-id":21665,"id":"Q21665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881097$A681EF04-07E4-4EA4-A333-0BFEAF91AE0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881097$60D9599E-6EC9-4826-9354-AEB4728872C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881097$98C4A411-B9BD-4361-8923-10A44A776C98","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":"Q2881097$4843135A-9558-4E7C-A14B-C82922C0C6F2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bfd2b71f82618261d5aaa3185617d5ee9df98463","datavalue":{"value":{"text":"On irrelevance and algorithmic equality in predicative type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2881097$23D9CB6C-9200-4329-80BF-AAA2442E9A80","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3ec1bc88c780d0b5c92400e3167000d28f157898","datavalue":{"value":{"entity-type":"item","numeric-id":3000599,"id":"Q3000599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6be9934386f5cca39f65a0a1c578bc244325c6dc","datavalue":{"value":{"amount":"+0.8967129588127136","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":"Q2881097$F79AB168-1B29-4B30-A859-82C407FF1BCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9fdc387bd755386d5018226729b82d32c15d7b1f","datavalue":{"value":{"entity-type":"item","numeric-id":5854731,"id":"Q5854731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ba3249e288e43001e5f29a8239bb11e85b108fb","datavalue":{"value":{"amount":"+0.7872315645217896","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":"Q2881097$C36285CB-6FEF-4867-8F67-3E7DBA6BA074","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0374978b71ce4f934a36d4ae8d192493815b5b6c","datavalue":{"value":{"entity-type":"item","numeric-id":3613437,"id":"Q3613437"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"622829b73f30b09b0b22a1a7237e07826dfb66b7","datavalue":{"value":{"amount":"+0.7363452911376953","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":"Q2881097$BC80AF3D-AF0E-4E75-8638-1540217C7925","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad8400280694217f7467aa7b38aa90d07462da14","datavalue":{"value":{"entity-type":"item","numeric-id":3003322,"id":"Q3003322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c55e1cb71a5d0a58193533be77ccb2e45720590","datavalue":{"value":{"amount":"+0.7361781597137451","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":"Q2881097$287B5758-FA79-4C04-8E20-B260A5D41F2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bf6171f0b09d240cdab1c5988ac08fee2e637217","datavalue":{"value":{"entity-type":"item","numeric-id":3637183,"id":"Q3637183"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c45f661157a619c4ba661ba763b622d84f125e6","datavalue":{"value":{"amount":"+0.7361778020858765","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":"Q2881097$D70563CC-9378-4563-BD5B-B2722EA48FFF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2881097","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2881097"}}}}}