{"entities":{"Q6535795":{"pageid":14146938,"ns":120,"title":"Item:Q6535795","lastrevid":55592251,"modified":"2026-02-17T19:22:59Z","type":"item","id":"Q6535795","labels":{"en":{"language":"en","value":"Impredicative encodings of inductive-inductive data in Cedille"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7810547"}},"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":"Q6535795$49F4B3C3-BAB8-41ED-82CD-A07465AAE7F1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2e1b50f23c6744fe41f9ce1194bbaa8c0cdb5164","datavalue":{"value":{"text":"Impredicative encodings of inductive-inductive data in Cedille","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6535795$1DB42C1A-2918-4B9D-897E-5D2CED901B02","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d64c9f174f6a26fb538bf703ba3919e8e15727a6","datavalue":{"value":"1547.68104","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535795$4FA8CF8E-1F1A-4DD5-B216-2D29B7C9AA69","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bf9943a99365954313e00aee636d805acb032689","datavalue":{"value":"10.1007/978-3-031-38938-2_1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535795$0DC40949-7B32-4E2D-9DC5-286608B0223A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d89e96d6b905e71d2e9d92e7766112115bf0a0d5","datavalue":{"value":{"entity-type":"item","numeric-id":5098732,"id":"Q5098732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$D03505C9-A896-462E-8F0B-8F40D0B1DC3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f81395139838cac6197cd512f660083e88955db5","datavalue":{"value":{"entity-type":"item","numeric-id":5020622,"id":"Q5020622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$C2FE0C14-55DA-4CAF-BA25-5E2D804582F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7daa8e19dd762c08a3fe86309cfbf3893a62423c","datavalue":{"value":{"entity-type":"item","numeric-id":286782,"id":"Q286782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$80CE7091-E6B4-46FC-9DB7-2B9F3076BF95","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1952080acac824c5abaf90b4ba5029824c97690c","datavalue":{"value":{"time":"+2024-02-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6535795$85F7836F-4242-44B1-823A-3C5C7F594A2D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535795$CE0417C5-8C38-40D8-8EF5-EE179767C114","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ee83bc8d225e0d0b9055aa57ab1e913a0028301b","datavalue":{"value":"7810547","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535795$5BBE21E3-873E-4687-9BB5-1204B25856E7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc969a139461dbee03dd0557722f0200f0b6db6a","datavalue":{"value":"impredicative encoding","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535795$4BE8943C-1194-452C-96E7-099E72D0F948","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01773f7fa3bae9013080dff115142d79035ecb95","datavalue":{"value":"induction-induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535795$7B8FFBAC-D352-4B55-8C67-ABF1F8A34980","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93914ef09ae1b2928c4a800314244e42dacf5175","datavalue":{"value":"Cedille","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535795$A961F0F6-23A9-4FA3-8726-38098873708C","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":"Q6535795$71862438-29E3-43A7-844F-20C8CFFA5479","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f33bf517641d12fc4df4d7fdbda832f3ef440e8b","datavalue":{"value":{"entity-type":"item","numeric-id":865639,"id":"Q865639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$C33E61C1-DBBB-4137-8C87-509AAA3D90B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d10e46b1e0cfb4bb12a7ff92b5fe74e9b2afacba","datavalue":{"value":{"entity-type":"item","numeric-id":1652995,"id":"Q1652995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$2B203F30-8A8E-4B30-B3B5-DA150F48DD5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"015256e4360c025094b2ad5c855ea10121fc5943","datavalue":{"value":{"entity-type":"item","numeric-id":3090862,"id":"Q3090862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$E05D98B8-539D-4D5F-B795-6642DB578558","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8324ecf1b83629f49a2cf02432ea440e2d5e9d22","datavalue":{"value":{"entity-type":"item","numeric-id":5145276,"id":"Q5145276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$2BB31FA0-1E73-44A5-BA06-3D891285BD15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5765b1c70da77537c6e225225ff527afc50bcc4e","datavalue":{"value":{"entity-type":"item","numeric-id":4263867,"id":"Q4263867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$5F922E6E-4D4C-4057-AC8C-7D87780B8D13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e6e84dc7d2442795960d241851cf13bc84741e4","datavalue":{"value":{"entity-type":"item","numeric-id":1412830,"id":"Q1412830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$A18BE779-BD42-440A-A365-58E3E38FF465","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"220e7bd07cfc86bd56365fb168aa15481d8c02d7","datavalue":{"value":{"entity-type":"item","numeric-id":2577476,"id":"Q2577476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$D8D496AB-85B7-40B0-B45B-2AEBAB1CDB28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42005bb3116815354c4371b0da1229b09744f2c2","datavalue":{"value":{"entity-type":"item","numeric-id":1791163,"id":"Q1791163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$EE7AD7C7-6873-4BDC-9DFB-D4A3D54C79BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"615fa71f9ac381c1b1417bf5e79adb133d890653","datavalue":{"value":{"entity-type":"item","numeric-id":2848936,"id":"Q2848936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$0DCBA604-8B6F-40C0-B706-F43F747B7F6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c837da3da6e1cce5954a238d7224430a5af53c4","datavalue":{"value":{"entity-type":"item","numeric-id":4981449,"id":"Q4981449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$D8AC81B9-094F-4B7E-AB86-D1970F35DC64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8eadddf82feaf866848bc8cb4dd929adcda9009d","datavalue":{"value":{"entity-type":"item","numeric-id":2778821,"id":"Q2778821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$4D7941DC-3C7F-45F6-8418-762F78534A16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d883e8a301f9d9a1270f265bcc8f905803e1f963","datavalue":{"value":{"entity-type":"item","numeric-id":5300900,"id":"Q5300900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$27D581DB-8364-421C-89E8-19DFF38935A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e9f241d35c9a7ff2bd599e2720c36ddf46ea63a2","datavalue":{"value":{"entity-type":"item","numeric-id":5098733,"id":"Q5098733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$1A78E8BB-502F-425D-88F9-7A93A6A53112","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37af35dc090c6c2687abaac50a4d7bcc03df7884","datavalue":{"value":{"entity-type":"item","numeric-id":6079233,"id":"Q6079233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$CE21C4BD-9763-4CCC-8947-F6BEAA25DD7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b28d48517ea43dcf1dc2bbbada71a7d7b49291bd","datavalue":{"value":{"entity-type":"item","numeric-id":2778831,"id":"Q2778831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$96F6F095-910A-4BB9-A0BE-1D6FF6F181C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13d920966bfcf66a9fc379fe82026a955fb20d53","datavalue":{"value":{"entity-type":"item","numeric-id":3586059,"id":"Q3586059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$A4DCD2DB-EED7-4DE5-B557-7F0749BD4A9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0882b92509d86167082a58bce5848b4bbe9f50ea","datavalue":{"value":{"entity-type":"item","numeric-id":4268477,"id":"Q4268477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$4FC49386-4CA7-42B5-A2A8-EE9BCB3ECDBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"980de19aad36b35085980c3806cdf17c9c9c82b8","datavalue":{"value":{"entity-type":"item","numeric-id":5372010,"id":"Q5372010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$E157CA91-16BF-415F-AC97-CF528F5E3516","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22130529177978d51b41ad2c5cdd3582a80fb3dd","datavalue":{"value":{"entity-type":"item","numeric-id":2636522,"id":"Q2636522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535795$7EF6DAEC-12AE-48DC-BC56-5585FCB68ECB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"512fbd36e27741965404e29ed9ad22c82889f878","datavalue":{"value":{"entity-type":"item","numeric-id":1791163,"id":"Q1791163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3c19e276dd782afb19722ab970b2ea96404c89be","datavalue":{"value":{"amount":"+0.7671591639518738","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":"Q6535795$22B754B9-A813-4FAB-9AAD-B267015A7B02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0544bace577260bd8bf794a56e7f472ad0511b0e","datavalue":{"value":{"entity-type":"item","numeric-id":5145279,"id":"Q5145279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"94dfef9d005381867fc50646152716c0bc9982e2","datavalue":{"value":{"amount":"+0.757138192653656","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":"Q6535795$19697A80-A579-4ECF-AEAD-E41C668C7A59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3a66d2cbfaf3c4e6c1901b9fd3ccb0f17582079","datavalue":{"value":{"entity-type":"item","numeric-id":5020623,"id":"Q5020623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3b1939d8711a5cc862cdc6021c11f9542ec429f","datavalue":{"value":{"amount":"+0.7547974586486816","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":"Q6535795$D9E400BF-0A7E-4AA5-85E9-3F6A049B3E75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"94ed348b0a35c2a6bf56c4bce9f1bd324eddbb65","datavalue":{"value":{"entity-type":"item","numeric-id":3090862,"id":"Q3090862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"932c56dc6d9101d9564c64af9e81f2519ddd5529","datavalue":{"value":{"amount":"+0.7250950336456299","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":"Q6535795$BFAB6CC7-7810-4C7D-8D69-BAE954529C5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c8230434b2ad6f33d1fc7cc0b757354a137c6c3","datavalue":{"value":{"entity-type":"item","numeric-id":5076393,"id":"Q5076393"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"de534fbc8923362e8df70d16242f1902ecee636e","datavalue":{"value":{"amount":"+0.6975218057632446","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":"Q6535795$FBF400D2-6FCB-483E-A5E8-4D51D896817A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6535795","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6535795"}}}}}