{"id":7033,"date":"2020-02-16T19:02:00","date_gmt":"2020-02-16T18:02:00","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7033"},"modified":"2020-02-16T19:02:00","modified_gmt":"2020-02-16T18:02:00","slug":"resena-mac-lanes-comparison-theorem-for-the-kleisli-construction-formalized-in-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-mac-lanes-comparison-theorem-for-the-kleisli-construction-formalized-in-coq\/","title":{"rendered":"Rese\u00f1a: Mac Lane\u2019s comparison theorem for the Kleisli construction formalized in Coq"},"content":{"rendered":"<div id=\"content\">\n<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre teor\u00eda de categor\u00edas titulado <a href=\"https:\/\/link.springer.com\/article\/10.1007%2Fs11786-020-00450-8\">Mac Lane\u2019s comparison theorem for the Kleisli construction formalized in Coq<\/a><\/p>\n<p>Sus autores son<\/p>\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/ekiciburak.github.io\/\">Burak Ekici<\/a> (de la <i>\u0130stanbul K\u00fclt\u00fcr University<\/i>) y<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/cek\/\">Cezary Kaliszyk<\/a> (del <a href=\"http:\/\/cl-informatik.uibk.ac.at\/\">Computational Logic Group<\/a> en la Universidad de Innsbruck).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>(co)Monads are used to encapsulate impure operations of a computation. A (co)monad is determined by an adjunction and further determines a specific type of adjunction called the (co)Kleisli adjunction. Mac Lane introduced the comparison theorem which allows comparing these adjunctions bridged by a (co)monad through a unique comparison functor. In this paper we specify the foundations of category theory in Coq and show that the chosen representations are useful by certifying Mac Lane\u2019s comparison theorem and its basic consequences. We also show that the foundations we use are equivalent to the foundations by Timany. The formalization makes use of Coq classes to implement categorical objects and the axiom uniqueness of identity proofs to close the gap between the contextual equality of objects in a categorical setting and the judgmental Leibniz equality of Coq. The theorem is used by Duval and Jacobs in their categorical settings to interpret the state effect in impure programming languages.<\/p><\/blockquote>\n<p>El trabajo se ha publicado en <a href=\"https:\/\/link.springer.com\/journal\/11786\">Mathematics in Computer Science<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas se encuentra <a href=\"https:\/\/github.com\/ekiciburak\/ComparisonTheorem-MacLane\/tree\/completeProof\">aqu\u00ed<\/a>.<\/p>\n<\/div>\n<div id=\"postamble\" class=\"status\">\n<p class=\"author\">Jos\u00e9 A. Alonso<\/p>\n<p class=\"date\">2020-02-16 dom 19:07<\/p>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre teor\u00eda de categor\u00edas titulado Mac Lane\u2019s comparison theorem for the Kleisli construction formalized in Coq Sus autores son Burak Ekici (de la \u0130stanbul K\u00fclt\u00fcr University) y Cezary Kaliszyk (del Computational Logic Group en la Universidad de Innsbruck). Su resumen es (co)Monads are used to&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7033"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=7033"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7033\/revisions"}],"predecessor-version":[{"id":7034,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7033\/revisions\/7034"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7033"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7033"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7033"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}