{"entities":{"Q5369482":{"pageid":7399056,"ns":120,"title":"Item:Q5369482","lastrevid":52930433,"modified":"2026-01-23T20:20:32Z","type":"item","id":"Q5369482","labels":{"en":{"language":"en","value":"The independence of Markov's principle in type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6792350"}},"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":"Q5369482$DB595C03-E356-43DD-9820-EB1DF07C7DDE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2de9fbf4738a5a5d7fb8d688ea2079c917f40b26","datavalue":{"value":"1434.03137","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369482$0A01ADE2-7ED6-4E94-BC91-74622AB0006E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5aad179d365c253d181fa8115a831f46e7923370","datavalue":{"value":{"entity-type":"item","numeric-id":375196,"id":"Q375196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5369482$9F500AC1-D473-42E9-B4B6-3548E45C567E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"47ea6504d86a7b2bece6ba0c846fcd038e7b467c","datavalue":{"value":{"entity-type":"item","numeric-id":1675766,"id":"Q1675766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5369482$19583DAF-9BD4-433F-961E-F0C57AC1704C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eae4cdb5001296cfa1d627ad5453506a5832f064","datavalue":{"value":{"time":"+2017-10-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":"Q5369482$73B3F713-BC0E-4BE4-9BBA-3A5B75067A58","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369482$6D95F479-37F6-4AE7-9058-175EED2284A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369482$C193CBCD-987F-4FC1-8CA8-1B403CBA219B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"98885bd1c25b8006ce085f2a50fc8ac0c1b6bdcd","datavalue":{"value":"03E40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369482$5EA27EAE-88B0-46AC-BA4B-7B00078613A0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1a0ea3c0f8e4b4b649e8bef3e161797de79cba66","datavalue":{"value":"6792350","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369482$C82F254F-0855-4EB8-BD88-30C65FAFA546","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1b23248042bd506455f51600d00d7ec5443276f9","datavalue":{"value":"forcing","type":"string"},"datatype":"string"},"type":"statement","id":"Q5369482$78C37E7D-D3AE-47DF-8D82-A7812A6BC41E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13fd823fa813aa32375d6c4605d9195c2318674c","datavalue":{"value":"dependent type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5369482$5ACDF433-B7EC-44D0-A8F6-C2609AA410D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe5670a6c6d1baa39a0a64ff77e086b1c9f1694a","datavalue":{"value":"Markov's principle","type":"string"},"datatype":"string"},"type":"statement","id":"Q5369482$DD85EB32-A06D-4A5C-9E96-48DBA69C6291","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"08f1124b1f4453113a28d664ddf4824eea31b856","datavalue":{"value":"Cantor space","type":"string"},"datatype":"string"},"type":"statement","id":"Q5369482$976B5F17-8F06-40B4-B062-FC38491A71F8","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":"Q5369482$34216980-CCC4-4D2C-91FE-EC9AA25555CF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a5d8ba68a3dd7c1a91cb01f9a370ad44828108c1","datavalue":{"value":"https://dblp.uni-trier.de/db/conf/rta/fscd2016.html#CoquandM16","type":"string"},"datatype":"url"},"type":"statement","id":"Q5369482$47BD10A8-6D68-4A2F-8187-63B40638C5A9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0bbfdaa4826c193f4de6f8665ee71b4858d53240","datavalue":{"value":"W2963610683","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369482$1E4F63EC-B4D2-44B8-A7E4-A08586E85534","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cd2a085da56811a4cea75611120c616c0d6e941a","datavalue":{"value":{"text":"The Independence of Markov's Principle in Type Theory.","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5369482$10523718-02A2-4D71-9384-7E2740890122","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"aa37d376d339bc91b730e37d1510190a695b0a79","datavalue":{"value":"10.4230/LIPICS.FSCD.2016.17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5369482$E6DDEA3E-9752-4A71-9294-AAE2AFBC5C0E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"09ddb2867c0a50fe3dc29b51467b1b79421042a9","datavalue":{"value":{"entity-type":"item","numeric-id":5367048,"id":"Q5367048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8cb2f692073bfe2c1595e5f3889942c954011831","datavalue":{"value":{"amount":"+0.9968119263648988","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":"Q5369482$70047831-03F4-45F2-BF26-6EE5C89A6F8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aac915318740a2078727118e33a25c1f76f36806","datavalue":{"value":{"entity-type":"item","numeric-id":4783332,"id":"Q4783332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9d0bc0061bd636caf9fe920fa99206c831007b1d","datavalue":{"value":{"amount":"+0.8445383906364441","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":"Q5369482$3F7EEC99-7036-4B06-870A-8026EB8453A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3bb1606410e789aa34a85f618dd2954e94a12d7c","datavalue":{"value":{"entity-type":"item","numeric-id":3315508,"id":"Q3315508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9d8a72cba4efaf67e259b1d4c8411119c83582c0","datavalue":{"value":{"amount":"+0.7467052936553955","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":"Q5369482$8579E847-161C-4ECE-939E-23D3A5BD5229","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"618df18a457f377baea80530122d19c937de0cc3","datavalue":{"value":{"entity-type":"item","numeric-id":3535125,"id":"Q3535125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d6cb84875ef6d98c6406e8db6baee9955a109573","datavalue":{"value":{"amount":"+0.7372518181800842","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":"Q5369482$F0103B5A-CA75-4CAB-881A-5384D5DD7A28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1d2a328de4393a6138737f57d51c482eacdb107","datavalue":{"value":{"entity-type":"item","numeric-id":2277259,"id":"Q2277259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b46d1a67d7cfba7dcc905a1893f0f914ef71f081","datavalue":{"value":{"amount":"+0.7371317148208618","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":"Q5369482$3ED33517-0D7F-4E14-880C-910814375BE2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5369482","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5369482"}}}}}