{"entities":{"Q5041060":{"pageid":7070637,"ns":120,"title":"Item:Q5041060","lastrevid":54419654,"modified":"2026-01-26T19:11:36Z","type":"item","id":"Q5041060","labels":{"en":{"language":"en","value":"Equality checking for general type theories in Andromeda 2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7600897"}},"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":"Q5041060$A3D496F4-6F2A-4BD3-8FF9-6467A7F57FBB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"691b910b51f2babb4480a1321722236a61c3d2c0","datavalue":{"value":{"text":"Equality Checking for General Type Theories in Andromeda 2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5041060$F707B143-3B7A-4D73-84EA-AA4E9B333090","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"253d231e736d46c1f6fecafb09eee6e130d6b080","datavalue":{"value":"1503.68287","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5041060$EE706EA4-4684-43D0-8925-CB4C4AC17157","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f30bc9e8e442047bf044c07105229d406027da32","datavalue":{"value":"10.1007/978-3-030-52200-1_25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5041060$D7FD6870-57FE-4779-B5F2-C958876D436E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0f2df3919dd6f0285578bf9d7f4189831f0dfe16","datavalue":{"value":{"entity-type":"item","numeric-id":390413,"id":"Q390413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041060$95173582-EBBD-4585-ADA4-7AF312928B67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fca977d035491d735c1acfaf289fd3ab39b041ce","datavalue":{"value":{"entity-type":"item","numeric-id":5041058,"id":"Q5041058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041060$BF602C5D-1BA8-4078-BE60-C8402BDE57D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6431594886ee232027e5010b84fff0ef0a05b0f2","datavalue":{"value":{"entity-type":"item","numeric-id":5041059,"id":"Q5041059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041060$E0B92DF8-72F0-4DFC-A65B-7DB0DC89CAE5","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041060$BE1C72C9-DAC1-4E38-9B66-E706B67C6346","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f63eb77a6cdb61f75205564f776cc43c0ac4bb43","datavalue":{"value":{"time":"+2022-10-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5041060$50589AF5-003B-4C48-8BA9-3770965AFB10","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5041060$85C53C52-A127-4660-A64D-6AD07F82477C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5041060$2ACC05C3-E1FF-40ED-AE8B-901E4FEDBA3E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f65c132d75ddc6d74e033666a460e7bbbe0f5059","datavalue":{"value":"7600897","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5041060$C983EBC8-25B4-4121-AC2E-5A7D0C64EEA3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"227553126e4bedd85da3837570904e989078e340","datavalue":{"value":"algorithmic equality checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q5041060$66257FAD-F242-439C-957F-82D2CE316569","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13fd823fa813aa32375d6c4605d9195c2318674c","datavalue":{"value":"dependent type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5041060$44600CF4-08AC-4629-A753-1903132DC1A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q5041060$8A4A2CF2-ACB2-44A3-8C6B-66BA01A0BA96","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"39d1d25ae8c00cfad058b188db36fd61dac09925","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041060$C4D72658-D093-438E-8D7D-8930ADE608FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041060$229A160C-435B-4A23-9421-6887A1B42248","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":"Q5041060$1EA9C0E6-853A-4FF6-9275-89169BA543AF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"99bfbf3460471cff223164c4a05151948cf73f80","datavalue":{"value":"https://doi.org/10.1007/978-3-030-52200-1_25","type":"string"},"datatype":"url"},"type":"statement","id":"Q5041060$688A2188-F7C2-4C7A-AE16-050EC0FAB808","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"87e95551bb267d75d06c8e8f541170a6467f1b2e","datavalue":{"value":"W3041607292","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5041060$0BBFDE52-4D29-4A57-BFA2-2DE432176C31","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"833079337a3c2f303ddbc3fe894c26799c99160e","datavalue":{"value":{"entity-type":"item","numeric-id":2881097,"id":"Q2881097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041060$65447BCB-A9CD-42F4-810B-FC193AB0E23D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"161e57333b0aa15cb58bedc63f47ab0c9d4e78fd","datavalue":{"value":{"entity-type":"item","numeric-id":5094888,"id":"Q5094888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041060$70A99510-59A2-45E4-B51D-1DC1972E0E87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c9a8987a7d8efa9b320ab9f4c18049ee75db52c","datavalue":{"value":{"entity-type":"item","numeric-id":4457464,"id":"Q4457464"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041060$C4BC9BD3-A282-48C9-8686-7FBDE794FF70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041060$7E8307D7-83AA-4F41-BF54-91D480B07D23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d284d3472d35d2cc3b63390bb184a9355795123","datavalue":{"value":{"entity-type":"item","numeric-id":4617969,"id":"Q4617969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041060$B0E0E9EA-402E-4325-9D97-A2BF1D0F040B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69fe664aa22c6ba1ea6d9ba12c2b4c3da0298ee2","datavalue":{"value":{"entity-type":"item","numeric-id":5277760,"id":"Q5277760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041060$425B4DC3-948D-4CB7-9DB4-34313096F6F8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a16a5f952fe65580ad3102001ed35bf577f03a9a","datavalue":{"value":{"entity-type":"item","numeric-id":5028472,"id":"Q5028472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c9eb9cb160df48a9509167bc1bb30ebdcadbd34","datavalue":{"value":{"amount":"+0.9050768613815308","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":"Q5041060$5274C18A-F46F-4CC7-B0AB-547B8695C22E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5688ed66a44257c423ffa0f6cb24d2c0a8e4433a","datavalue":{"value":{"entity-type":"item","numeric-id":4645754,"id":"Q4645754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"384827acdff78b8c78935f2f18780ce35558e20b","datavalue":{"value":{"amount":"+0.7249149680137634","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":"Q5041060$FAA67915-EA16-4A18-8CC5-BC6907647CDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"270de6527ae96c33d421a94a582ab741c9b0b3f7","datavalue":{"value":{"entity-type":"item","numeric-id":5705901,"id":"Q5705901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"646fdaf3b57c307998ac2f8a2593e54bc11fdaf1","datavalue":{"value":{"amount":"+0.7121134400367737","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":"Q5041060$35C29B91-9B00-49EF-8463-C74CEA1D2B58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e62e08aae69bf14a5dee004999b6c7f37287ffbc","datavalue":{"value":{"entity-type":"item","numeric-id":3521979,"id":"Q3521979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dd0545f815ce7ef8719d82699e857c27223a35d7","datavalue":{"value":{"amount":"+0.7058186531066895","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":"Q5041060$D17023C8-DE5C-499E-9EF8-632FDA6FC1AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"60f3045a8a306759da1455f1710e78fb89afaf15","datavalue":{"value":{"entity-type":"item","numeric-id":3593498,"id":"Q3593498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"62c3527581b023cc848bfd862431ccb7e068550b","datavalue":{"value":{"amount":"+0.7054579854011536","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":"Q5041060$D1E0AC97-DF11-4A70-93E6-B0E031BF6DE2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5041060","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5041060"}}}}}