Reseña: Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq

Se ha publicado un artículo de razonamiento formalizado en Coq sobre teoría de categorías titulado Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq

Sus autores son

Su resumen es

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

El trabajo se ha publicado en Mathematics in Computer Science.

El código de las correspondientes teorías se encuentra aquí.

José A. Alonso

2020-02-16 dom 19:07