{"entities":{"Q5145670":{"pageid":7175241,"ns":120,"title":"Item:Q5145670","lastrevid":94606979,"modified":"2026-06-05T07:14:51Z","type":"item","id":"Q5145670","labels":{"en":{"language":"en","value":"Large and infinitary quotient inductive-inductive types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7299502"}},"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":"Q5145670$909AD8EA-7CA2-4EA9-A07B-21C910C2E501","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"25244bb4b2d92dfa2618689d77477b65135c8269","datavalue":{"value":{"text":"Large and Infinitary Quotient Inductive-Inductive Types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5145670$708251BC-3FFA-4694-BE09-DA51B32DA0ED","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ae83de02e2e8c7e9762af27b2e8ff6a1bd71e026","datavalue":{"value":"1498.03032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145670$BC9CD5A9-9CA0-4CEB-BBA8-D76A045CD989","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"980aff6bc1362d82b3a4f8fc99bbf6998a74176f","datavalue":{"value":"10.1145/3373718.3394770","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145670$2BFAA9E3-89CE-4534-BDAD-20B34DD05063","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"08ce0e0cdedd491f2be40b586710d257b049396c","datavalue":{"value":{"entity-type":"item","numeric-id":421064,"id":"Q421064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5145670$C69DC1CD-72CB-4959-B3CD-7EE8AD251F4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a7cbc48b481a6b830ab14eacad20738b43bab2e0","datavalue":{"value":{"entity-type":"item","numeric-id":2176676,"id":"Q2176676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5145670$A7DD09E5-B672-478A-BCC9-BF27C9E52D64","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":"Q5145670$D463008F-E845-4E81-944D-D51B4D01EC68","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":"Q5145670$8016D55B-AB2B-4867-994B-B62F104354A0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8936f72fbdaa05a39da25c89b52229cf2fd2babf","datavalue":{"value":"https://arxiv.org/abs/2006.11736","type":"string"},"datatype":"url"},"type":"statement","id":"Q5145670$81CD15B9-A894-485E-807A-05BA86962AC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P205","hash":"834a746f105bdf94416e28721e43c8b22459e28d","datavalue":{"value":"http://real.mtak.hu/112924/1/2006.11736.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q5145670$847F084B-697C-40DD-BA47-BBBB5E1C1D4E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145670$569C5D82-ABF4-4456-BD23-58C094055271","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7e484257c74fd4d77f4c561fae766838a1692cbd","datavalue":{"value":"7299502","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145670$05A3D7D4-7CBD-48A6-B177-750DE8C00DBE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4d5793ae76a4a96f8ae785ef4f3cf3d0157b4fb5","datavalue":{"value":"categories with families","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145670$B1C82193-31C4-417D-83A6-955AF1C5F737","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e1202fa4aaeffc809043c1d94983ad89396bca2","datavalue":{"value":"inductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145670$8F485159-5F81-40F9-AA13-908DFA41E56D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"006b7ad344dd553f4779c349586aa8780144d141","datavalue":{"value":"infinitary inductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145670$12B958F0-E3D3-4C06-9FF8-8B9B9A6AC468","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"102491f62699dab3eb36e7105844a34fc822bb98","datavalue":{"value":"quotient inductive-inductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145670$701816A9-943A-4EAF-ABED-D89518847417","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":"Q5145670$770513E2-7E30-46AA-AE0D-F5960B997D5B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c054fda31d771a45875ffd137f385fa856a78f8c","datavalue":{"value":"W3028596397","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145670$7B5C82CF-1645-4972-B079-230DCCFADCA2","rank":"normal"}],"P1643":[{"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":"86c9f202150ae981c141eccc79f98ada2bf0d1c4","datavalue":{"value":{"amount":"+0.8201885223388672","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":"Q5145670$33F069ED-1E57-4C3D-A072-9AEE7E3BC0AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80eee57571fdbb56a12fbb8fc8ab44a57cfd5c63","datavalue":{"value":{"entity-type":"item","numeric-id":5094144,"id":"Q5094144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6801a434ad4a84a0557c79b84e9f519eab69bf6a","datavalue":{"value":{"amount":"+0.8165303468704224","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":"Q5145670$779DCE72-F780-4831-AE73-CBBEF96553E2","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":"027409411916e7a018a397ac598ca4d0b795d06b","datavalue":{"value":{"amount":"+0.797693133354187","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":"Q5145670$BB1CF0B2-DF22-46AF-AF5A-A65DA5685F4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46d5eb500b91b900b7e0ec167e7c875fd9ecd2d8","datavalue":{"value":{"entity-type":"item","numeric-id":2828239,"id":"Q2828239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"813773e422b126286def80905088f529d64b1e4a","datavalue":{"value":{"amount":"+0.7769646644592285","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":"Q5145670$12F0EF49-EC0A-4F49-A203-5FFD3C522F09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d5045d469091b2aad0fb30f11c21619d52a0114","datavalue":{"value":{"entity-type":"item","numeric-id":4993350,"id":"Q4993350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7add304ea3ecb0bd75f84eb5e3e01865e0c11e0b","datavalue":{"value":{"amount":"+0.7245954871177673","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":"Q5145670$B23E3427-7D56-44BA-A1E6-B946DB3DD29E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Large and infinitary quotient inductive-inductive types","badges":[]}}}}}