{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T00:19:03Z","timestamp":1722471543068},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2020,2,8]],"date-time":"2020-02-08T00:00:00Z","timestamp":1581120000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,2,8]],"date-time":"2020-02-08T00:00:00Z","timestamp":1581120000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"University of Innsbruck and Medical University of Innsbruck"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Math.Comput.Sci."],"published-print":{"date-parts":[[2020,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats: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<jats:italic>uniqueness of identity proofs<\/jats:italic>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.<\/jats:p>","DOI":"10.1007\/s11786-020-00450-8","type":"journal-article","created":{"date-parts":[[2020,2,8]],"date-time":"2020-02-08T09:03:04Z","timestamp":1581152584000},"page":"533-549","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Mac Lane\u2019s Comparison Theorem for the Kleisli Construction Formalized in Coq"],"prefix":"10.1007","volume":"14","author":[{"given":"Burak","family":"Ekici","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,2,8]]},"reference":[{"issue":"1","key":"450_CR1","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1016\/j.jlamp.2014.02.001","volume":"84","author":"A Bauer","year":"2015","unstructured":"Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Log. Algebr. Methods Program. 84(1), 108\u2013123 (2015)","journal-title":"J. Log. Algebr. Methods Program."},{"issue":"2","key":"450_CR2","first-page":"409","volume":"1","author":"C Byli\u0144ski","year":"1990","unstructured":"Byli\u0144ski, C.: Introduction to categories and functors. Form. Math. 1(2), 409\u2013420 (1990)","journal-title":"Form. Math."},{"key":"450_CR3","unstructured":"Capriotti, P.: pcapriotti\/agda-categories. https:\/\/github.com\/pcapriotti\/agda-categories\/, (2014)"},{"key":"450_CR4","unstructured":"Carette, J., Hu, J., Stucki, S., Sebe, MO: agda\/agda-categories. https:\/\/github.com\/agda\/agda-categories (2019)"},{"issue":"4","key":"450_CR5","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1017\/S0960129510000150","volume":"20","author":"C Dom\u00ednguez","year":"2010","unstructured":"Dom\u00ednguez, C., Duval, D.: Diagrammatic logic applied to a parameterisation process. Math. Struct. Comput. Sci. 20(4), 639\u2013654 (2010)","journal-title":"Math. Struct. Comput. Sci."},{"key":"450_CR6","doi-asserted-by":"crossref","unstructured":"Dumas, J.-G., Duval, D., Fousse, L., Reynaud, J.-C.: Decorated proofs for computational effects: States. In: Golas, U., Soboll, T. (eds.), Proceedings Seventh ACCAT Workshop on Applied and Computational Category Theory, Tallinn, Estonia, 1 April 2012, Vol.\u00a093 of EPTCS, pp. 45\u201359 (2012)","DOI":"10.4204\/EPTCS.93.3"},{"issue":"4","key":"450_CR7","doi-asserted-by":"publisher","first-page":"719","DOI":"10.1017\/S0960129511000752","volume":"22","author":"J-G Dumas","year":"2012","unstructured":"Dumas, J.-G., Duval, D., Fousse, L., Reynaud, J.-C.: A duality between exceptions and states. Math. Struct. Comput. Sci. 22(4), 719\u2013722 (2012)","journal-title":"Math. Struct. Comput. Sci."},{"key":"450_CR8","unstructured":"Ekici, B.: Towards Mac Lane\u2019s Comparison Theorem for the (co)Kleisli construction in Coq. In: Proceedings of the 3rd FMM 2018, co-located with the 11th CICM (2018)"},{"key":"450_CR9","unstructured":"Gross, J., Chlipala, A., Spivak, D.I.: Experience implementing a performant category-theory library in Coq. In: Klein, G., Gamboa, R. (eds.), Interactive Theorem Proving\u20145th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14\u201317, 2014. Proceedings, Vol. 8558 of LNCS, pp. 275\u2013291. Springer (2014)"},{"issue":"10","key":"450_CR10","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"450_CR11","unstructured":"Ishii, H.: konn\/category-agda. https:\/\/github.com\/konn\/category-agda, (2013)"},{"key":"450_CR12","unstructured":"Jacobs, B.: A recipe for state-and-effect triangles. Log. Methods Comput. Sci. 13(2) (2017)"},{"key":"450_CR13","unstructured":"Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201988, pp. 47\u201357, New York, NY, USA (1988). ACM"},{"key":"450_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7","volume-title":"Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics.","author":"S Mac Lane","year":"1971","unstructured":"Mac Lane, S.: Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer, Berlin (1971)"},{"key":"450_CR15","doi-asserted-by":"crossref","unstructured":"McBride, C.: Elimination with a motive. In: TYPES, Vol. 2277 of Lecture Notes in Computer Science, pp. 197\u2013216. Springer (2000)","DOI":"10.1007\/3-540-45842-5_13"},{"issue":"1","key":"450_CR16","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"450_CR17","unstructured":"Peebles, D.: copumpkin\/categories. https:\/\/github.com\/copumpkin\/categories, (2018)"},{"key":"450_CR18","doi-asserted-by":"crossref","unstructured":"Plotkin, G.D., Pretnar, M.: Handling algebraic effects. Log. Methods Comput. Sci. 9(4) (2013)","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"450_CR19","unstructured":"Pouillard, N.: crypto-agda\/crypto-agda. https:\/\/github.com\/crypto-agda\/crypto-agda\/tree\/master\/FunUniverse (2015)"},{"key":"450_CR20","unstructured":"Timany, A.: amintimany\/categories. https:\/\/github.com\/amintimany\/Categories (2017)"},{"key":"450_CR21","doi-asserted-by":"crossref","unstructured":"Timany, A., Jacobs, B.: Category theory in Coq 8.5. In: Proceedings of the 1st FSCD, Porto, Portugal, pp. 30:1\u201330:18 (2016)","DOI":"10.1145\/3434288"},{"key":"450_CR22","unstructured":"Voevodsky, V., Ahrens, B., Grayson, D., et\u00a0al.: UniMath\u2014a computer-checked library of univalent mathematics. https:\/\/github.com\/UniMath\/UniMath (2018)"},{"key":"450_CR23","unstructured":"Wiegley, J.: jwiegley\/category-theory. https:\/\/github.com\/jwiegley\/category-theory (2018)"}],"container-title":["Mathematics in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-020-00450-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11786-020-00450-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-020-00450-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T09:37:27Z","timestamp":1722418647000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11786-020-00450-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,8]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,9]]}},"alternative-id":["450"],"URL":"https:\/\/doi.org\/10.1007\/s11786-020-00450-8","relation":{},"ISSN":["1661-8270","1661-8289"],"issn-type":[{"type":"print","value":"1661-8270"},{"type":"electronic","value":"1661-8289"}],"subject":[],"published":{"date-parts":[[2020,2,8]]},"assertion":[{"value":"30 November 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 December 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 February 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}