{"entities":{"Q5145279":{"pageid":7174850,"ns":120,"title":"Item:Q5145279","lastrevid":58456680,"modified":"2026-04-05T07:30:42Z","type":"item","id":"Q5145279","labels":{"en":{"language":"en","value":"Impredicative encodings of (higher) inductive types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7298732"}},"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":"Q5145279$1D481722-F648-47F9-986A-90EF39C093B3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bbaaaaade16a5dc5c8f5cda54456f4e1ed50cb0f","datavalue":{"value":{"text":"Impredicative Encodings of (Higher) Inductive Types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5145279$DF0D289D-E105-4854-968D-FEB231D74708","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"43dbfa0133a9b72fecc173160d872e92c151fa3b","datavalue":{"value":"1452.03030","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145279$7B9A5390-19C1-494E-B902-9638FFA38111","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"01120282bca559db165b8a8bef90db1e19f514cd","datavalue":{"value":"10.1145/3209108.3209130","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145279$78A500B8-AE56-4452-902C-61837977633B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9ca6076d2d4cf97e6395c92fd68e50d20bea8c46","datavalue":{"value":{"entity-type":"item","numeric-id":476120,"id":"Q476120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5145279$CFB2B57A-93B8-4C48-8D7D-B53A66B73E46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4b03f33de8edc8701c5386464eb82c47c87e7688","datavalue":{"value":{"entity-type":"item","numeric-id":5145278,"id":"Q5145278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5145279$1DB10126-F1DD-4690-9E35-A44659AE2743","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2009e276a9c17224dc798d13c148c747ba9f7376","datavalue":{"value":{"entity-type":"item","numeric-id":938240,"id":"Q938240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5145279$54C762D3-463F-408F-8F80-F46D94E948B8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ee82b0c640d35f6663be3f8a5187d8cc540da0b3","datavalue":{"value":{"entity-type":"item","numeric-id":5145269,"id":"Q5145269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5145279$87A418EA-099E-40A4-8C1F-598001207F9F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"233394734482eba32ed4ee15da745b1ac2b96149","datavalue":{"value":{"time":"+2021-01-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5145279$030261D1-5120-4A28-805B-B90A03289C16","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0fbe6da38c9b5325e6b0363834af23ef3aca1e44","datavalue":{"value":"https://arxiv.org/abs/1802.02820","type":"string"},"datatype":"url"},"type":"statement","id":"Q5145279$B8EE8B82-1A1D-4F3C-BE31-C9D85664BA2A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145279$A63E1ECD-5892-4C28-BAA3-59C6D422671E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"72047dd175f2df177aa1ddf4f7ca150e0c1e70c2","datavalue":{"value":"55U35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145279$B618063F-75E4-4FC0-9A2E-9B001D673044","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"befe607509a93d2a536d630fd3a8e8ae944f11b0","datavalue":{"value":"18N40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145279$E7F76BEC-939F-491F-AC32-BE07668AA271","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"342ab571402b7f72581bd59d5ba3f633043f8227","datavalue":{"value":"7298732","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145279$4CA748CB-B968-4F11-B5B9-227A2EB0E1A2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6886acc9bb720e6ad7ca13e49d3bd87570dc950","datavalue":{"value":"higher inductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145279$99D88134-EC44-4B4A-9125-51FF05FCB454","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4ecd2d433c9f863c39fe5a1fa2de24434b6de0d","datavalue":{"value":"homotopy type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145279$4F35F61A-B72A-427F-9580-87073EAAE560","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"38f3161bfff7ede888bfcd0be8e5e4973957d942","datavalue":{"value":"impredicative encodings","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145279$316DF151-5F92-4281-A25F-B3894D84EBE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f5795787683dc16a0e892761f65c085daecc3346","datavalue":{"value":"impredicativity","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145279$0615DE15-DF38-4798-95DF-1093F41FEC73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e1202fa4aaeffc809043c1d94983ad89396bca2","datavalue":{"value":"inductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145279$0EE42C5C-C5D9-4AB5-A2E1-62090BB332B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"454090389315247a59dda8a7c520ea2795715012","datavalue":{"value":"Martin-L\u00f6f type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145279$5F35C095-5455-40D6-8248-B8D938C5DFBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"826cb17a61389397478ca005848e294acb35a0eb","datavalue":{"value":"system F","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145279$249B6D63-AB8C-4FBF-B38C-51C790FD6CFD","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":"Q5145279$DDF9BD0F-DEAA-4D72-96AF-FC21D3BC6B33","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"32b1ef2ef0dc25d6b390119d1064154345ee2120","datavalue":{"value":"W2963511234","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145279$44E7EA89-53FA-46A1-A566-72924508D4DA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e001309006a43b2c682ba66be212a39e7be2b26a","datavalue":{"value":{"entity-type":"item","numeric-id":4958656,"id":"Q4958656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ad4665ba54a3890ae6abf243678241e301813c54","datavalue":{"value":{"amount":"+0.7277796268463135","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":"Q5145279$575145DB-082D-4CF5-A5C9-FB9514E6FA56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"40128ae02f3139cea7e9c0e92b048dc1f467b01a","datavalue":{"value":{"entity-type":"item","numeric-id":4635920,"id":"Q4635920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71f062f1f3d99bc30631c23401510087ae36ca30","datavalue":{"value":{"amount":"+0.7146387100219727","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":"Q5145279$39667BC5-3A2B-47D8-8CA6-AF9D5A4F2007","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b229fdf3be6e29888a59c1cd99bc0786aab224e","datavalue":{"value":{"entity-type":"item","numeric-id":556819,"id":"Q556819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"77b594bfaf16b175ed695b891bcda0afb3f3c74a","datavalue":{"value":{"amount":"+0.7140662670135498","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":"Q5145279$51A6667F-8680-40A3-A447-14197C7465AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2a1ccb3b200eacff668c56085d8ceadba2ef59b","datavalue":{"value":{"entity-type":"item","numeric-id":5145298,"id":"Q5145298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8ed0c348ba81730cc6549d21a9325a942a3b88f2","datavalue":{"value":{"amount":"+0.7076326608657837","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":"Q5145279$0E1B2267-FD62-4BA1-89EA-A69E75EA8904","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cdfd99d9c223eb0f3fc5e26de01873d6f72966b3","datavalue":{"value":{"entity-type":"item","numeric-id":4364399,"id":"Q4364399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1897a0b14c9af1e76d426788376c802c2dee0123","datavalue":{"value":{"amount":"+0.70365971326828","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":"Q5145279$F3989311-4928-46D1-BE67-5224420B45CB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5145279","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5145279"}}}}}