{"entities":{"Q5277827":{"pageid":7307402,"ns":120,"title":"Item:Q5277827","lastrevid":58509771,"modified":"2026-04-05T13:00:10Z","type":"item","id":"Q5277827","labels":{"en":{"language":"en","value":"Non-wellfounded trees in homotopy type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6744142"}},"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":"Q5277827$D1DF1113-9D84-4AA4-B4CE-A01306FB62CD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bc1c253cf54eb759652a4bd5e019331948232d65","datavalue":{"value":"1433.03027","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5277827$39D66FE2-4828-45C2-81F2-9DD739AD377D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ebdd912b169a139b5481c76e8978f5a1ad20396","datavalue":{"value":{"entity-type":"item","numeric-id":2319988,"id":"Q2319988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5277827$C05651A4-1511-45CF-8101-6250F553BEEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"725426ba4e3e8b8ec62a89eadeb43219fbf11018","datavalue":{"value":{"entity-type":"item","numeric-id":1652992,"id":"Q1652992"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5277827$F2BA2C67-DB3B-41A4-A775-48F3E7289712","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"01a790b95f0c9c8094b25d95f4830f54baf58560","datavalue":{"value":{"entity-type":"item","numeric-id":2945652,"id":"Q2945652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5277827$8651A60E-407C-4EBC-9566-B9623B6C8075","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"da4ed36bae8b600bf66a15aabe0c472becc2ce16","datavalue":{"value":{"time":"+2017-07-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5277827$78C7F574-C1A3-4265-9B2D-C8D5D7737555","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"af98829513b11d7f999f67cea0785ebaa3f33d88","datavalue":{"value":"https://arxiv.org/abs/1504.02949","type":"string"},"datatype":"url"},"type":"statement","id":"Q5277827$B8B1BB21-CD1F-4040-B1C8-3D99665887BA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5277827$D2A6675B-101A-4464-B9DD-B6521352813C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5277827$9D152123-5AE6-40FA-B66D-9F8182607F4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"72047dd175f2df177aa1ddf4f7ca150e0c1e70c2","datavalue":{"value":"55U35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5277827$0522A0B0-C642-40BF-B06F-82FAF7C5BF21","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ffdf2dfde498077c66228fc50a2f6cfb906691c0","datavalue":{"value":"6744142","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5277827$62733B29-4312-4234-80EF-EAE35D7E72FA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4ecd2d433c9f863c39fe5a1fa2de24434b6de0d","datavalue":{"value":"homotopy type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5277827$86D8EDCC-B5E2-4B00-AEF0-FE699D961E20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0aec078788f97936bc6f63bf4e3ce60ecba5c3dd","datavalue":{"value":"coinductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5277827$28306DA3-AB6F-4646-85D4-87C12F3E7A9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7501fcc2fe56cf5a562014ad3157969001677d88","datavalue":{"value":"computer theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5277827$801183D9-0449-44F6-A696-9487A8AE7269","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5277827$C794EF53-9B97-4EFE-BDF6-08376A3905D5","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":"Q5277827$7518AC58-2243-4CF1-8447-04465D59884C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"467b26caf9feeb9ab382f6b9a9321e9beed28c4c","datavalue":{"value":"10.4230/LIPICS.TLCA.2015.17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5277827$CDE3AC10-89A4-46DC-BDB4-30F32A91AFFE","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":"1440a4efafccfc9991c9ce0314cedb13e65267f2","datavalue":{"value":{"amount":"+0.8042272925376892","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":"Q5277827$9CF2B464-E2A2-4EB8-95DD-B4F86D31AC79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f96a820e5c47e2953e18031df9f9fd72c084a01","datavalue":{"value":{"entity-type":"item","numeric-id":2819787,"id":"Q2819787"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b26ef68781961e75960021644c56a0f508ad60d","datavalue":{"value":{"amount":"+0.7553035020828247","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":"Q5277827$8914ACFF-5A5A-40AF-8FFB-524128418621","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6e2fa711171a0ac47274caeed4c6108ca6294c1","datavalue":{"value":{"entity-type":"item","numeric-id":2933829,"id":"Q2933829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7322ab27f84dc76b9c736989de56aa43d54c8ee2","datavalue":{"value":{"amount":"+0.7474802136421204","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":"Q5277827$E30AF1AA-4A58-4EA3-85AB-3F4F414D69DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c58a42b478ce3b79ea5fc5be5cf0b55cb50e8490","datavalue":{"value":{"entity-type":"item","numeric-id":2957700,"id":"Q2957700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"815c5f2974b4678035e38d9925050258a7d056de","datavalue":{"value":{"amount":"+0.7468776702880859","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":"Q5277827$9D963DBB-C8D5-43C9-B322-6B1B53B67F3D","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":"9f3ec6551e16dc5a8c51ecbe86ea1696125fb83f","datavalue":{"value":{"amount":"+0.7429067492485046","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":"Q5277827$EBACEBBE-2CEE-4986-AF33-5690F37D0034","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5277827","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5277827"}}}}}