{"entities":{"Q627204":{"pageid":629052,"ns":120,"title":"Item:Q627204","lastrevid":63074100,"modified":"2026-04-11T10:25:35Z","type":"item","id":"Q627204","labels":{"en":{"language":"en","value":"Map fusion for nested datatypes in intensional type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5853826"}},"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":"Q627204$6368C51E-5BC4-4654-910F-3FAAAB420593","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6ab38277b40bf0034a9dc1a87b4bb609c8f44677","datavalue":{"value":{"text":"Map fusion for nested datatypes in intensional type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q627204$677BB097-6F75-4FF9-AFB7-8386FD79D310","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8e3b0566304cb6b3efe6a288c7745fcdc3bd7c7f","datavalue":{"value":"1210.68048","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q627204$C85CFF72-71BB-454C-A02B-C5AAFB534B03","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0f31cf0ba649c82a71b5cbd30114eb63bfddbeed","datavalue":{"value":{"entity-type":"item","numeric-id":627203,"id":"Q627203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$EA4CAC48-C8DC-41FF-973D-B97BD7063037","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4082512e7d3530b9726df691c7c28e9fec542a8c","datavalue":{"value":{"entity-type":"item","numeric-id":169675,"id":"Q169675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$FAB87281-BBAF-4916-A83B-4A61EF63ED43","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a57a1d265a3ee40f730aaa4d5af28fb13b1a54e5","datavalue":{"value":{"time":"+2011-02-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":"Q627204$ECCE59E0-3D5C-4FF5-BFC6-A79444259D64","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q627204$AB806A29-5922-4629-AC07-8B135A24E9D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q627204$EF81AE49-85A0-453A-92E6-EB3EC71877BD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c328edb789bd84c12c7aed24801d0174496a03a4","datavalue":{"value":"5853826","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q627204$FD318B2E-EB26-47C5-8363-552B4C767C63","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q627204$C2D39FCF-0D87-47E9-B89C-875E056469A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q627204$4E736355-4136-42EC-AFB3-3D919683E4C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2ef3959e85acbbcd91dc790b2c05d72b2058d951","datavalue":{"value":"datatypes with true nesting","type":"string"},"datatype":"string"},"type":"statement","id":"Q627204$46B11913-EC6C-4130-A401-84ED51347680","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b626a8fbcf294a5399b0127991833b4b514e7a84","datavalue":{"value":"naturality for generalized maps","type":"string"},"datatype":"string"},"type":"statement","id":"Q627204$51078D04-185F-4A11-823B-B65EAB193025","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50b90852db9c96ee6e5451852da9cb32bdfb4636","datavalue":{"value":"explicit flattening","type":"string"},"datatype":"string"},"type":"statement","id":"Q627204$A48A385A-3E4E-4C30-9551-B3DE3BCC797B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f73f524d0522b107d8c3cc0a27500f101ba0ec2d","datavalue":{"value":"monad laws for substitution","type":"string"},"datatype":"string"},"type":"statement","id":"Q627204$1CDCFB91-57A4-4CA1-A13B-D8DFDBD04399","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"834cdda0dc4fb8ca955aff1476a94851f7884f7e","datavalue":{"value":"terminating recursion schemes","type":"string"},"datatype":"string"},"type":"statement","id":"Q627204$A88E39D2-A7C6-4554-BA7B-617D3B7CCDAA","rank":"normal"}],"P1463":[{"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":"Q627204$14A81E92-C46C-4810-B17C-1388E5D7C2F5","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":"Q627204$3BEC2D45-BD28-4288-B916-936582ED9C36","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"02deeaf2cf27ff5cde603f5dc8ba8ddca4208417","datavalue":{"value":"https://doi.org/10.1016/j.scico.2010.05.008","type":"string"},"datatype":"url"},"type":"statement","id":"Q627204$C72BFBDB-8939-4236-9214-DE28DCCE0D24","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f0c65844eb07aa4f9d12c4dcec2ed73d291bf8d9","datavalue":{"value":"W2018045457","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q627204$43280AB7-4131-4DC5-9B3A-D20DA08ACE8F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f2109afedce1b483ee7fc2708dbda6319653a96","datavalue":{"value":{"entity-type":"item","numeric-id":4519172,"id":"Q4519172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$D76E99BA-3E17-4A66-B5F6-D1D12750CA9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a1c4e3e9abb8d3f1418514c061c1d7ea6d5d61f","datavalue":{"value":{"entity-type":"item","numeric-id":1346686,"id":"Q1346686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$C70C9AAB-685F-4523-B691-DE50100887C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a797407b4949355fcd06204fe2bcb7b1218a925","datavalue":{"value":{"entity-type":"item","numeric-id":4256148,"id":"Q4256148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$FA04E5B3-5A37-46F7-8382-110FE41AF3D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c541a0e0fccb98a32f18a8695d9eabb1926b39f3","datavalue":{"value":{"entity-type":"item","numeric-id":4945244,"id":"Q4945244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$36FDCCB3-637F-46A6-AC61-2D918D7DF5F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6be1541264ec7f3427f16feb9f0814ae8b381955","datavalue":{"value":{"entity-type":"item","numeric-id":848745,"id":"Q848745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$C32A2539-04C8-49A7-B55C-5D87C71FEB50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$0F6ACA6F-8378-4E67-A38E-3A28D094E87B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bb1812a83c3a4aee25d6a67b2527c143aea9ae4","datavalue":{"value":{"entity-type":"item","numeric-id":4435471,"id":"Q4435471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$D1E6D1CE-E0F0-479C-8356-4C5B17554E43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"150719399e882b786834d79969b3d0373e1dfbae","datavalue":{"value":{"entity-type":"item","numeric-id":1770412,"id":"Q1770412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$9920A21E-A118-4FD5-AA2F-DF59C04F8D25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a17422820de131ed03dd36bb6484e8aa078aa9e","datavalue":{"value":{"entity-type":"item","numeric-id":1965249,"id":"Q1965249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$35788021-D1A2-454A-9EB0-ADF59AFE2891","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea00778f52ec611b9197a1255baadb7b2fd0cf06","datavalue":{"value":{"entity-type":"item","numeric-id":4435457,"id":"Q4435457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$1EB8073B-9C97-4145-86F4-F5E8ED6F4D40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15f915bd6752b8e731b62673178ee8eafb7e0b32","datavalue":{"value":{"entity-type":"item","numeric-id":4331824,"id":"Q4331824"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$7C0EF604-BA31-4ABB-8132-9FD40F4A805E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58137c2009742a39b30e5cb42aa06402d77c473a","datavalue":{"value":{"entity-type":"item","numeric-id":3638923,"id":"Q3638923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$413BE15B-6EAB-4E74-80A5-CA6D260B8A91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a19e38fbc8f9f8c11b9ab7ad79f464c27504bd57","datavalue":{"value":{"entity-type":"item","numeric-id":1882785,"id":"Q1882785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$A4275878-FCB6-467E-A7D4-CA56695DFA4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7339740287f50f43f28bfb905009c15405396d84","datavalue":{"value":{"entity-type":"item","numeric-id":3521990,"id":"Q3521990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$451EB30A-DC33-4D61-91AD-C73F74AF9C0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26dac06384dc787a405949068340510a6602af80","datavalue":{"value":{"entity-type":"item","numeric-id":4463991,"id":"Q4463991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$97BD322B-013A-4495-B6FE-7013B6C1BBAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e8e358264bd4fafb5ae8fe354ce3b216cca1b18","datavalue":{"value":{"entity-type":"item","numeric-id":5311256,"id":"Q5311256"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$71D05891-E556-48FA-AA21-514041B80921","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b948850fe331e2b203a34ee2a1cc029dc3504fe4","datavalue":{"value":{"entity-type":"item","numeric-id":3507459,"id":"Q3507459"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$708702C0-68A5-40F1-BC5C-B2F5BE510AA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bdf4ccdcc70e71d35fd15b371cfa64eecb3f47f9","datavalue":{"value":{"entity-type":"item","numeric-id":4215784,"id":"Q4215784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$DF2A02FD-A6B4-42CC-ADA6-6814DC7BB6B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"364525b70d80e5ad032dd4bcb752b39f36195669","datavalue":{"value":{"entity-type":"item","numeric-id":4508246,"id":"Q4508246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q627204$579A7C8B-5567-4E9B-9135-556A9F51D7B5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1b22f4850cb25bb60d791d43dac79dfe6f91f2b2","datavalue":{"value":"10.1016/J.SCICO.2010.05.008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q627204$7FE236CB-D3AA-4975-ABCF-0D30F89D3880","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51b78ba281286c1cc0ddf52fabe91d14b7284261","datavalue":{"value":{"entity-type":"item","numeric-id":3521990,"id":"Q3521990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f92dc4bfd540605cd7ea13172d4bd69a4002032","datavalue":{"value":{"amount":"+0.8774302005767822","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":"Q627204$61311ABE-C465-451A-808A-1252AA2CE419","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e96e5ab9adf8e1f1051043588a3b7b879c09e039","datavalue":{"value":{"entity-type":"item","numeric-id":3638923,"id":"Q3638923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8782500088742cb781ab3335a9ccc1e1c33bb54","datavalue":{"value":{"amount":"+0.7972568869590759","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":"Q627204$A58736BC-9CB6-4A79-A8A3-0CCCAF06B9B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8481af880417872a6aa16122fd2b04cd7ce47b4d","datavalue":{"value":{"entity-type":"item","numeric-id":1770412,"id":"Q1770412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"41df76b8cb48e4d541a134bcf54e29da6e997653","datavalue":{"value":{"amount":"+0.779084324836731","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":"Q627204$94B3D76E-7A44-4DFC-9DD7-CDACF7BA041E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0f7f90919181d7fd39fe7ee9f5f53d1191d927ec","datavalue":{"value":{"entity-type":"item","numeric-id":3507459,"id":"Q3507459"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78686173198aa4a51a194d82daec982b34102018","datavalue":{"value":{"amount":"+0.7742354869842529","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":"Q627204$23FD56B7-6EB3-4FAA-AD09-E6E81D350039","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3528211c656f8da22dd5d08de4791f6b65975fb1","datavalue":{"value":{"entity-type":"item","numeric-id":4417851,"id":"Q4417851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a12e4f8cfdef25974ec4c9b310d72e746754da72","datavalue":{"value":{"amount":"+0.7668969631195068","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":"Q627204$EEA5622E-0E50-4B6F-A0D0-2B371F0FD27C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Map fusion for nested datatypes in intensional type theory","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Map_fusion_for_nested_datatypes_in_intensional_type_theory"}}}}}