Person: EKİCİ, BURAK
Loading...
Email Address
Birth Date
Research Projects
Organizational Units
Job Title
Dr. Öğr. Üyesi
Last Name
EKİCİ
First Name
BURAK
Name
1 results
Search Results
Now showing 1 - 1 of 1
Publication Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq(Springer, 2020) EKİCİ, BURAK; Kaliszyk, Cezary(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.