{"entities":{"Q3000599":{"pageid":3011323,"ns":120,"title":"Item:Q3000599","lastrevid":51249206,"modified":"2026-01-17T10:56:06Z","type":"item","id":"Q3000599","labels":{"en":{"language":"en","value":"Irrelevance in type theory with a heterogeneous equality judgement"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5897362"}},"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":"Q3000599$56881013-F8AA-4974-A29C-20AA5C423DC1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"405e050f672466a6267626d9e439e77504fe25c2","datavalue":{"value":{"text":"Irrelevance in Type Theory with a Heterogeneous Equality Judgement","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3000599$758CA8FE-B2E4-41E0-BEBF-59D055A24280","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"af6d3c1f7e47548ebbef2c2a330a9c7361cb237d","datavalue":{"value":"1326.68076","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3000599$5A977E93-2AEE-40C2-B95B-8BFF79D752AE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"42bc69c1d8bb8c65acf13a27a583fd90b5eb73a5","datavalue":{"value":"10.1007/978-3-642-19805-2_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3000599$833CF1B0-ABB6-4778-A5CA-E8DB5F55E0A7","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":"Q3000599$D3E05DE4-868F-442B-A62E-AA2312E0A2DE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"24804f4b3014a48e696dd6005da1c061736a75ea","datavalue":{"value":{"entity-type":"item","numeric-id":2892754,"id":"Q2892754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3000599$C6D18C38-1490-486F-9A5A-D959227DDB0E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"07154ee076353c2b0adec8e531d763756f4412f7","datavalue":{"value":{"time":"+2011-05-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3000599$24BA512B-27CB-4DFC-92F0-D8E6D47F463E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3000599$5963F666-BF34-4E86-BC29-431F184ACA54","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"12bec8d0b9d1e5be477a19641642108b8a1966c1","datavalue":{"value":"5897362","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3000599$4487F979-A51C-487E-A4F2-3125414D3769","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q3000599$9F276684-480D-46AD-89E7-BCDB47ED9142","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fda5d8057392e50193b0eca80d9562ae727873ec","datavalue":{"value":"proof irrelevance","type":"string"},"datatype":"string"},"type":"statement","id":"Q3000599$9BE43B64-E461-4747-9365-98D7F625EE3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93dab88d8daf807f9d46d6fa3c07545e9aac6cbe","datavalue":{"value":"heterogeneously typed equality","type":"string"},"datatype":"string"},"type":"statement","id":"Q3000599$2B29F6C3-0E5A-4519-B270-4A1BB39552D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b821c17356860e1d19b5594261acde7c321d71b","datavalue":{"value":"algorithmic equality","type":"string"},"datatype":"string"},"type":"statement","id":"Q3000599$7F4A5FD5-E26F-4AC6-A3C2-D2788CC0EA2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fd09c797952a268ece59feabb30b339489339461","datavalue":{"value":"logical relation","type":"string"},"datatype":"string"},"type":"statement","id":"Q3000599$B169C49B-068D-484A-8A5B-A52EF1C79279","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2a3c42e92edacb9578ee7aa6e6989b083d06b242","datavalue":{"value":"universal Kripke model","type":"string"},"datatype":"string"},"type":"statement","id":"Q3000599$BC8F4526-6465-424A-BDE2-0C47879F73F7","rank":"normal"}],"P1463":[{"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":"Q3000599$E3F0B875-EFDF-449D-9DFA-CCA6F0533FEB","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":"Q3000599$6ABF8EC7-253C-4066-8947-0C24DB03F0A6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8e523e78c829fa9596d5c2c7986ac8249d517fdb","datavalue":{"value":"https://doi.org/10.1007/978-3-642-19805-2_5","type":"string"},"datatype":"url"},"type":"statement","id":"Q3000599$F23EEEDD-4A7F-4353-8C93-F3A34AF8A0B7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c2da6b1b186956293046765c6e77c027f8defb62","datavalue":{"value":"W1515341800","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3000599$D72D45CC-0CA7-45CB-9BC7-F92A1490EFAF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5de30d754af82d7575c5218ddb8f50be80efb2ac","datavalue":{"value":{"entity-type":"item","numeric-id":2881097,"id":"Q2881097"},"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":"Q3000599$B1EA17E9-AA58-4C03-9677-2777812DF903","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":"785418a5eae3b71358b3dd5a0eaa1cd90185789a","datavalue":{"value":{"amount":"+0.8402961492538452","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":"Q3000599$E3E5FBC8-4E6A-4AF2-9424-28FF53A5391E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca4128576115585c6eeba0ae32dedbf5d93cb852","datavalue":{"value":{"entity-type":"item","numeric-id":3535620,"id":"Q3535620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"57cf58dc4362786a1975235555260ff0e8490e64","datavalue":{"value":{"amount":"+0.7336748838424683","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":"Q3000599$B217BA6D-1A5B-4826-BE6B-B707AECECB31","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":"a3107e88d7a7917478a8b5b5cca0eced4ea541d2","datavalue":{"value":{"amount":"+0.7331063747406006","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":"Q3000599$883C5B73-9C4D-4FC6-8348-E9CCBEED423C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5632702bf3390b03ea1bb4daaa31ca609d002f89","datavalue":{"value":{"entity-type":"item","numeric-id":5145355,"id":"Q5145355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e0931c3c3b4823e8626d75acef393126c4e7a6a3","datavalue":{"value":{"amount":"+0.726651668548584","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":"Q3000599$E9A2026A-1E3C-436E-AFCC-ECA20528402D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3000599","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3000599"}}}}}