{"entities":{"Q2333322":{"pageid":2344065,"ns":120,"title":"Item:Q2333322","lastrevid":71868993,"modified":"2026-04-14T01:04:43Z","type":"item","id":"Q2333322","labels":{"en":{"language":"en","value":"Formalization of universal algebra in Agda"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7128698"}},"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":"Q2333322$FD767789-F4BC-4CE8-9857-56FD531C339A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ddfafd00a3c9fe76f10d63dd520d90b7e9d118e8","datavalue":{"value":{"text":"Formalization of universal algebra in Agda","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2333322$C35F6C61-39D6-4A97-A0EC-8C8899D5CAFB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2df11cc67e6dda58bc0ff23e67ca4df5cbff8900","datavalue":{"value":"1433.68578","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333322$DC37BDBA-417B-422D-A984-B7FFC06CFBF6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"352e58e2c56f4ce94f212d36f5b3e137785644f0","datavalue":{"value":{"entity-type":"item","numeric-id":2333320,"id":"Q2333320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$AA05D72B-0D7A-4DBF-84AC-02EAD632BE86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e9c4be091d1286ce12b2e39fd704f492aac49f72","datavalue":{"value":{"entity-type":"item","numeric-id":2333321,"id":"Q2333321"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$5684E865-EF7B-4CA0-9E10-92BD5A844D0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"09573ab70c9d986235750625015542077d5f5980","datavalue":{"value":{"entity-type":"item","numeric-id":1744421,"id":"Q1744421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$D2C6A6A6-5677-4C15-A3E3-18975A6DBDDE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"38a671beb2eece257f68ae67ea5951ace27cbec7","datavalue":{"value":{"time":"+2019-11-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":"Q2333322$030833C9-6325-4BD4-BDD5-9D392B74BAFC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333322$5A25FA95-D86A-40D6-A77E-4F951DED0216","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed4ac44229a63771ae4ded31038fe93f434bffb7","datavalue":{"value":"03C05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333322$CDD7FA08-EA10-4545-84B2-4A9CDFA96E12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333322$06498AC1-1E5F-4AB7-9E71-7E9CA2E0F72A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fa6b2a062a1000d772fed673ce2f8cc8e8a49c79","datavalue":{"value":"7128698","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333322$4874AACE-AF4F-482E-BBBA-A7B9FFD0D2B1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09a188bc590546995974b55a3f2f84f00e08b2a9","datavalue":{"value":"universal algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333322$DA7EEADD-0D4C-4CBD-9915-8D1A442AA05D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"658126897c7f6bf3db78fea48b2876524c1d8c9e","datavalue":{"value":"formalization of mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333322$118A22B8-ED52-4F7E-8E9E-335FFFB4137A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"744fd5f6b592344bd2a87ac1816bb7847861172e","datavalue":{"value":"equational logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333322$01ABA230-C44F-4BFC-A4C4-B393AA73C37A","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"d1aaf6079d73df07343079a7c52bab44487eac69","datavalue":{"value":"Q113317505","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333322$7CCA9427-A16E-4C1A-BC49-5B208A93250B","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":"Q2333322$E51B0308-577F-43FA-B678-A3C02ADBF475","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":"Q2333322$3BD3BB37-5BE4-4B2C-B2B5-1C6F26AE0128","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"40820da74bac94a7c09241b50509634d0eae39c0","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2018.10.010","type":"string"},"datatype":"url"},"type":"statement","id":"Q2333322$5C9E3CF2-30F5-463B-A8E0-D646CAF5B627","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6dd41d506ff84253b0076f972966b25ac6482380","datavalue":{"value":"W2898803326","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333322$CA396BBF-26A5-46E5-846A-590056EFEE4A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"79aa05cbdf7e9c30715a43e649084cfac28e9645","datavalue":{"value":{"entity-type":"item","numeric-id":4457833,"id":"Q4457833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$79B3E9AB-B7F8-4485-83FA-35CB53B5EF2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e2db18f956a86c51893ceffc869b394629d46fd","datavalue":{"value":{"entity-type":"item","numeric-id":5611775,"id":"Q5611775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$594036D7-7AE9-4B12-9CC7-F333224DB20C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1903be4a36187a0a0e197e708bc72f62f93b28bd","datavalue":{"value":{"entity-type":"item","numeric-id":3183520,"id":"Q3183520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$FADC317B-6073-4EF9-9E09-9C35267FA3DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab8ea372caa817f188e4e943a4cbc2ab55cc9d12","datavalue":{"value":{"entity-type":"item","numeric-id":5549412,"id":"Q5549412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$18D470E3-F481-4FC6-8017-E4FDEC671FDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e3205f61ab0cf0c757b93cbb15b5f9dfc288bf4","datavalue":{"value":{"entity-type":"item","numeric-id":4945205,"id":"Q4945205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$0A100AD2-CB71-410F-AEA1-A2A136AB4C46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab2f872f7b124497811cc27de7d8d98a7f30bb1f","datavalue":{"value":{"entity-type":"item","numeric-id":3656423,"id":"Q3656423"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$F1F9889A-E87C-4EE9-AB50-5528311465A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd265bdbcf41f2b9982b655d7aaf44e4072217fa","datavalue":{"value":{"entity-type":"item","numeric-id":4692630,"id":"Q4692630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$9A30CBB6-8C4C-4561-9A87-10BCD7D57BBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd6cd0d0c72bd63bb035b0e71b44baff47cc10e6","datavalue":{"value":{"entity-type":"item","numeric-id":3586098,"id":"Q3586098"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$EB314791-3360-4ED9-81B4-E28B46312B9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ae708d8b20f899dd2270716c7b5874f1659ff49","datavalue":{"value":{"entity-type":"item","numeric-id":3269195,"id":"Q3269195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$8762D06A-3675-48FC-ACA9-BE44216166B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85438f12b2728ba9c19aea71f3be4f00937583b1","datavalue":{"value":{"entity-type":"item","numeric-id":3347940,"id":"Q3347940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$06DC2E3F-CE3E-4176-803C-5A80C1CC2F83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3dcf6718201adb615b8978d3b59187bbe61f55f","datavalue":{"value":{"entity-type":"item","numeric-id":3493234,"id":"Q3493234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$6ECDC4EE-C8D7-413C-9D1E-3A01F4055246","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"443ade8344e996017f9036639debfb0f18f67baf","datavalue":{"value":{"entity-type":"item","numeric-id":4302820,"id":"Q4302820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$7795A28E-FA55-4AE4-BF6B-B937B05B1787","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"46bd0d834cbcc25e715dac95fc7fe23da36cae4e","datavalue":{"value":{"entity-type":"item","numeric-id":3012523,"id":"Q3012523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$A7727CEC-F15F-4DC9-BDA7-F9A47F8199F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9c583b65c7819a91d7f03c50f27e11283eee826","datavalue":{"value":{"entity-type":"item","numeric-id":3962973,"id":"Q3962973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$606B7D77-C758-4487-A9E8-A1486F84B721","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0065dc8b5c25773ef1d9719266c7992d0edd4dd5","datavalue":{"value":{"entity-type":"item","numeric-id":4131619,"id":"Q4131619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$A43F3D74-D7BE-479D-921E-11CCC01E16D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7dac16af6cf1adb18d0516e2c8db27f45fc424e6","datavalue":{"value":{"entity-type":"item","numeric-id":5327343,"id":"Q5327343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$5F058DF8-CCE3-4791-A78A-B166B9C3CC28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b2e6d6d678c66a8f67b32f0421bc8641276b0bcd","datavalue":{"value":{"entity-type":"item","numeric-id":1129121,"id":"Q1129121"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$89E95112-BD8D-4440-888F-49D7A9C083D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf22f682016f944ff79f619b0dece60771cb1f03","datavalue":{"value":{"entity-type":"item","numeric-id":3007580,"id":"Q3007580"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$1E1E9009-CBFF-4985-BDF7-E8CC5BC84AA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19bc50e2f4d2cceaac2ab96d0b4ab028848b7d4b","datavalue":{"value":{"entity-type":"item","numeric-id":4023900,"id":"Q4023900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$3798F665-9A67-4737-A6A2-FCD75A238559","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68846a18ed55aeabe9d47edb1111eca82c571bda","datavalue":{"value":{"entity-type":"item","numeric-id":2787340,"id":"Q2787340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$27A266D0-37D1-46AC-8394-33CDF1BE89EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cddef8b5bd5f5c14fec95d2275f181b3acadcc5","datavalue":{"value":{"entity-type":"item","numeric-id":3498425,"id":"Q3498425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$B766BB38-707A-4697-86C2-CD0456E60B30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a1fec13708686f567ce8f652a4b4b1f5722daf5","datavalue":{"value":{"entity-type":"item","numeric-id":610397,"id":"Q610397"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$0E131C4B-EB00-42B5-9E53-06E2B1D8E882","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26a98ca8ad947d93065e67feb1362da03cdb7848","datavalue":{"value":{"entity-type":"item","numeric-id":3094177,"id":"Q3094177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$716E749D-C532-4C14-BBDA-B3483B3D3BE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"46025091f572832566b89fd22ecee091f86ae10d","datavalue":{"value":{"entity-type":"item","numeric-id":4904107,"id":"Q4904107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$B65D839C-67C4-4139-894F-13D4875E7AF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"02a8f5ca257597984bc40adebcc761ca0d5d76ae","datavalue":{"value":{"entity-type":"item","numeric-id":1156472,"id":"Q1156472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$2E822872-B578-42FD-BBAB-B4A339CF2E57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f27d1cf41ec859f2924aead3f46b262dc817ff6","datavalue":{"value":{"entity-type":"item","numeric-id":3377761,"id":"Q3377761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333322$DB32C4BB-2588-4B8B-8C9E-97588C03C6AC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d99aa91d3bcf7221a1509b9eae485c1489f76f33","datavalue":{"value":"10.1016/J.ENTCS.2018.10.010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333322$59F560F0-7663-422A-A510-29B348400CA5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0cdcd388e89d00caee1fc23e4f3bb301c9a3516f","datavalue":{"value":{"entity-type":"item","numeric-id":3007580,"id":"Q3007580"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b9763727bd5dc9b16a7306b047419857535b6b7","datavalue":{"value":{"amount":"+0.7452917098999023","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":"Q2333322$7920086A-4BE6-4B29-BA9B-5FAE88555374","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b0d0dddb42a37c084a843d2425ab699fcd5eace1","datavalue":{"value":{"entity-type":"item","numeric-id":5271090,"id":"Q5271090"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"616471d2dacfc7c44878c6810e75db6d615f0aad","datavalue":{"value":{"amount":"+0.7330963015556335","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":"Q2333322$2EA2FDEE-570C-4641-8AE4-B06C7B22814F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f283ce1b7bb222e202a6acf28a6a844d9018de04","datavalue":{"value":{"entity-type":"item","numeric-id":5747673,"id":"Q5747673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"84b5de1f90bbf311213734497de93921e992dcac","datavalue":{"value":{"amount":"+0.7289429306983948","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":"Q2333322$FABB5176-556D-44EC-AF4B-B171119CE3B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"da51a64ce85b824c0c6a00156958187439a882fc","datavalue":{"value":{"entity-type":"item","numeric-id":2319990,"id":"Q2319990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c63879d93775da6f681d6acc12752aa5aad703d0","datavalue":{"value":{"amount":"+0.7131969332695007","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":"Q2333322$2504FEE0-DF2C-43EE-9C0B-E1BAB4E33C10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d2297eb8442881cd6208ce70d13682d01272971","datavalue":{"value":{"entity-type":"item","numeric-id":5145623,"id":"Q5145623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78245ddbee0b4d38838ae594613555a0aaa94784","datavalue":{"value":{"amount":"+0.7111133933067322","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":"Q2333322$3EF0621E-BCAE-4137-9741-C9D7056D11FF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization of universal algebra in Agda","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_of_universal_algebra_in_Agda"}}}}}