Publication:
Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq

Loading...
Thumbnail Image
Date
2020
Authors
Kaliszyk, Cezary
Journal Title
Journal ISSN
Volume Title
Publisher
Springer
Research Projects
Organizational Units
Journal Issue
Abstract

(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's 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.

Description
Keywords
Adjunctions , Monads , Kleisli Construction , Comparison Theorem , Coq
Citation
Ekici, B., & Kaliszyk, C. (2020). Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq. Mathematics in Computer Science, 14(3), 533-549.