{"entities":{"Q5145619":{"pageid":7175190,"ns":120,"title":"Item:Q5145619","lastrevid":94606538,"modified":"2026-06-05T07:14:47Z","type":"item","id":"Q5145619","labels":{"en":{"language":"en","value":"The integers as a higher inductive type"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7299459"}},"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":"Q5145619$D381C6D4-E7F5-4594-B3F7-9D7276FEC856","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0f199302f7f43875507ee0d127cfcdc5b623df32","datavalue":{"value":{"text":"The Integers as a Higher Inductive Type","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5145619$2F97B1AE-1C76-4AA7-9E2D-25C5BA4CCA45","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"22f23cac64d6e317c3114615a1cb6a5046ae3900","datavalue":{"value":"1498.03028","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145619$766B8B25-D76A-4891-B49A-FFB701676814","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e7f2409d33d4456fbcf27c0d3a690315202b14e4","datavalue":{"value":"10.1145/3373718.3394760","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145619$38486E57-48E9-4225-9CE9-9BC69EC8DAE3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6801a503eb1bea2102d1e59832005afa5cab1cee","datavalue":{"value":{"entity-type":"item","numeric-id":1652991,"id":"Q1652991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5145619$1CD76DF9-A9B9-4754-ACAB-2182D7A88B31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ca821cdd87eb9515180f49adf70233ecd22c013f","datavalue":{"value":{"entity-type":"item","numeric-id":5139289,"id":"Q5139289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5145619$DFBADDC7-0F3D-4FDA-9B96-8DD99D0DAEDE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d6acabd1d03c7bf4038f1fe09f6b50384b32deb5","datavalue":{"value":{"entity-type":"item","numeric-id":5145612,"id":"Q5145612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5145619$218EE267-F35F-4CDA-877C-EEAA522871F5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2be4cfc06a63d907ae95fa44423b78da0f5c0eb3","datavalue":{"value":{"time":"+2021-01-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5145619$41971461-188B-4BE0-A6A4-E37C53D2E67C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f83f08632ce4d1f0dc1c6854ab529481e334613f","datavalue":{"value":"https://arxiv.org/abs/2007.00167","type":"string"},"datatype":"url"},"type":"statement","id":"Q5145619$D23C1AA7-6E9F-489A-B35D-4B0923E90B37","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145619$7C06D2B5-3B92-47F6-9F23-30DB2AD97FDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"72047dd175f2df177aa1ddf4f7ca150e0c1e70c2","datavalue":{"value":"55U35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145619$59CF900D-7C98-4CB3-867B-30A874F9867B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dc9a4660f4497e5f1d0102b9481bc1c28d08d790","datavalue":{"value":"18N45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145619$6D2254B6-D982-42A7-BCFC-EABBCC25F266","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"203e3ff324d1f1d473f6a2dd2009b4064db68de6","datavalue":{"value":"7299459","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145619$2C3712D7-C281-46C9-B5BF-A30D095E9CBE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0705a939195357c482458d36fda47eaa88b5dcb4","datavalue":{"value":"coherence problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145619$63F09680-65EC-4C6B-931A-DAC3BD4B8A2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab586850bffcc4762366730ad6f3984c02839e0b","datavalue":{"value":"higher inductive type","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145619$159819FB-B0CA-4884-B124-0CC1853AE187","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"92c715c998c2c4beeb41208853a051b29ca14e86","datavalue":{"value":"initiality","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145619$BAD82FBC-F80F-4D11-977F-6F354ECD54E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e0c50a94e462a143153bb7186bc384099ed023e","datavalue":{"value":"truncation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145619$818E741F-0DCC-4242-909F-7DD57553CFC5","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":"Q5145619$FFE9FB6A-9760-49AC-968D-901A66D09B5D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"25279f924152e8ce3d7468695a1be7680f4893aa","datavalue":{"value":"W3032285962","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145619$2E0571DB-A616-4703-8823-E73EA1924D20","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eceaac39afb5b5bf6071ca0d9d41e6a0697cba8e","datavalue":{"value":{"entity-type":"item","numeric-id":2986785,"id":"Q2986785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c69cd52286e99230cd165349bf98237f4849810e","datavalue":{"value":{"amount":"+0.7444661259651184","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":"Q5145619$29C4E8AE-3C79-4A5E-B063-B37D0CC17FD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a4d1b0501bc0ca62d393e5b76273a0ea507e928","datavalue":{"value":{"entity-type":"item","numeric-id":5420262,"id":"Q5420262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5050de5654cc113cc303cae805476c196e6927d9","datavalue":{"value":{"amount":"+0.7321631908416748","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":"Q5145619$D00FFE46-5E26-4232-9E3A-3B8BE85553EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a611ae37cd77e81d821a59e1af5afe2303c597fc","datavalue":{"value":{"entity-type":"item","numeric-id":1687770,"id":"Q1687770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"85b54edb0316ba66ab98ab9961556981fde693f9","datavalue":{"value":{"amount":"+0.7251071929931641","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":"Q5145619$BBCC5B22-928F-4F09-9BD6-CE1A2BA37A8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2ad3f7793c966f5800be0bc53668750d78d41f94","datavalue":{"value":{"entity-type":"item","numeric-id":5145692,"id":"Q5145692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f3bdeeac85d632712562456e5b8aad04a5985e6","datavalue":{"value":{"amount":"+0.7207231521606445","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":"Q5145619$482C086E-9BE9-4C5B-AFB9-C8D4DB2B5773","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aac67a273a6ae0afefb612f1d3784f5bcff8aa55","datavalue":{"value":{"entity-type":"item","numeric-id":1652995,"id":"Q1652995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6cdb02da0cd07dddb3c8bfdf5e6a8c5e563f08fe","datavalue":{"value":{"amount":"+0.7184453010559082","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":"Q5145619$9760A716-E914-45E3-899E-C9AA4D2DE39A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The integers as a higher inductive type","badges":[]}}}}}