This short paper summarizes an ongoing work on the formalization of Mac Lane's comparison theorem for the (co)Kleisli construction in the Coq proof assistant. Proposition 1.2. A hom-adjunction F a G : D ! C , with associated family of bijections ' as in De nition 1.1, determines a monad on C and a comonad on D as follows: • The monad (T; ; ) on C has endofunctor T = GF : C ! C , unit : IdC ) T where X = 'X; F X (idF X ) and multiplication : T 2 ) T such that X = G("F X ).
(1) (2) (3) • The comonad (D; "; ) on D has endofunctor D = F G : D ! D , counit " : D 'GA1; A(idGA) and comultiplication : D ) D2 such that A = F ( GA). ) IdD where "A = In addition, we have: 'X; Af = Gf 'X1;Ag = "A
X : X ! GA for each f : F X ! A
F g : F X ! A for each g : X ! GA: Proposition 1.3. Each monad (T; ; ) on a category C determines a Kleisli category CT and an associated hom-adjunction FT a GT : CT ! C as follows: C l , CT We give an overview below, please nd the related details in [ML71, Ch. VI, §5].
• The categories C and CT have the same objects and there is a morphism f [ : X morphism f : X ! T Y in C . So that there is a bijection de ned as: ! Y in CT for each ('T )X; Y : HomCT (X; Y ) =! HomC (X; T Y ) f [ [ f • For each object X in CT , the identity arrow is idX = h[ : X ! X in CT where h = X : X ! T X in C : • The composition of a pair of morphisms f [ : X ! Y and g[ : Y ! Z in CT is given by the Kleisli composition: g[ f [ = h[ : X ! Z where h = Z T g f : X ! T Z in C : • The functor FT : C ! CT is the identity on objects. On morphisms, • The functor GT : CT ! C maps each object X in CT to T X in C . On morphisms,
FT f = ( Y
f )[; for each f : X ! Y in C : GT (g[) =
Y
T g; for each g[ : X ! Y in CT : (4) (5) Theorem 1.4. (The comparison theorem for the Kleisli construction) Let F a G : D ! C be a hom-adjunction and let (T; ; ) be the associated monad on C . Then, there is a unique comparison functor L : CT ! D such that GL = GT and LFT = F , where CT is the Kleisli category of (T; ; ), with the associated hom-adjunction FT a GT : CT ! C . larly, let X; Y : HomD (F X; Y ) =! HomC (X; GY ) be a bijection associated to the hom-adjunction F a G. Since both units of FT a GT and F a G are the unit of the monad (T; ; ) by [ML71, Ch. IV, §7, Proposition 1], we obtain the commutative diagram below:
LFT X;Y X;Y = / HomC (X; GT Y ) idX;GT Y
= =
X;LY / HomC (X; GLY ) Therefore, LFT X;Y = X1;LY X;Y . This formula ensures that the functor L is unique. Using the Equation (2) in Proposition 1.2, we have: X;Y f [ = GT f [ X : X ! GT Y; for each f [ : FT X = X ! Y in CT : Since GT f [ = Y T f in C , for each f [ : X ! Y in CT , by Equation (5), we have X;Y f [ = Y T f X : X ! GT FT Y = GT Y: Thanks to the naturality of , we get X;Y f [ = Y T Y f . The monadic axiom
Y T Y = idT Y yields X;Y f [ = f : X ! GT Y . Presumed that GT = GL and since FT is the identity sointioonbj1ec.2t,s, wwee ohbatvaein X;XY1;fLY[ f= =f :"XLY ! FGfLY= a"nFdYLFTFYf == LYX1;F=Y fFfYo:r eNaocwh,f b:yXEq!uatGioFnY(3i)n iCn: PHroenpcoe
X1;LY ( X;Y f [) = X1;F Y f = "F Y F f: In other words: given a functor L satisfying GL = GT and LFT = F , then it must be such that LX = F X for each object X in CT and Lf [ = "F Y F f in D for each f [ : X ! Y in CT : We additionally need to prove that L : CT ! D , characterized by LX = X and Lf [ = "Y F f , is a functor satisfying GL = GT and LFT = F : A specialized version of the theorem is used by the author to model some formal logics in order to handle computational side e ects in his thesis [Eki15]. An alternative de nition of adjunctions is given in the following. De nition 1.5. Let C and D be two categories. The functors F : C ! D and G : D ! C form an adjunction F a G : D ! C i there exists natural transformations : IdC ) GF and " : F G ) IdD such that: "F X G"X
F X = idF X for each X in C
GX = idGX for each X in D (6) (7) Lemma 1.6. De nition 1.5 () De nition 1.1.
See the proof in [Hen08, §3, Theorem 3.5]. 2
In a Coq implementation1, we represent category theoretical objects such as functors, natural transformations, monads and adjunctions with data structures having single constructors and several elds, namely classes. This is no di erent than the approaches by Gross et al. [GCS14], Timany et al. [TJ16]2 and John Wiegley3. To our knowledge, none of them include the formalization of Mac Lane's comparison theorem. Also, our formalization makes use of proof irrelevance and functional extensionality axioms. These being said, let us start with the formalization of De nition 1.1:
Class HomAdjunction {C D: Category} (F: Functor D C) (G: Functor C D): Type , mk_Homadj
{ ob: @Isomorphism (FunctorCategory (D^op C) CoqCatT) (BiHomFunctorC F G) (BiHomFunctorD F G) }.
An instance of the HomAdjunction class is de ned as an isomorphism of bifunctors in the category of functors. In the above snippet, the notation D^ op denotes the dual of the category D, and CoqCatT represents the category of Sets. BiHomFunctorC implements the hom-functor HomC (X; GA) while BiHomFunctorD stands for the functor HomD (F X; A) in (1). On the other hand, De nition 1.5 looks like:
Class Adjunction {C D: Category} (F: Functor C D) (G: Functor D C): Type , mk_Adj { unit : NaturalTransformation (@Id catC) (Compose_Functors F G); counit: NaturalTransformation (Compose_Functors G F) (@Id D); ob1 : 8 a, (trans counit (fobj F a)) o fmap F (trans unit a) = @identity D (fobj F a); ob2 : 8 a, (fmap G (trans counit a)) o trans unit (fobj G a) = @identity C (fobj G a) }. 1https://github.com/ekiciburak/ComparisonTheorem-MacLane 2https://github.com/amintimany/Categories 3https://github.com/jwiegley/category-theory where unit and counit correspond to and " as well as proof obligations ob1 and ob2 implement Equations (6) and (7) respectively. This means that to build an adjunction out of given categories and functors, one needs to provide two natural transformations satisfying the obligations. In the script, fmap is a eld of the Functor type class that maps arrows while fobj is another eld of the same class mapping objects of a domain category; trans is a led of the NaturalTransformation class representing the component of the natural transformation at a given object. Id is the identity functor.
Formalizing in Coq Propositions 1.2, 1.3 and Theorem 1.4, we use Adjunction class instances instead of the ones of HomAdjunction. This is indeed not a problem thanks to Lemma 1.6. We have it certi ed in Coq: Lemma adjEq1: 8 (C D: Category) (F: Functor C D) (U: Functor D C), Adjunction F U ! HomAdjunction F U.
Lemma adjEq2: 8 (C D: Category) (F: Functor C D) (U: Functor D C), HomAdjunction F U ! Adjunction F U. We move on with the formalization of Proposition 1.2:
Theorem adj_mon : 8 {C D: Category} (F: Functor C D) (U: Functor D C), Adjunction F U ! Monad C (Compose_Functors F U).
Theorem adj_comon: 8 {C D: Category} (F: Functor C D) (U: Functor D C), Adjunction F U ! coMonad D (Compose_Functors U F). See Adjunctions.v le for the proofs of so far stated theorems/lemmas. We implement Proposition 1.3 in three steps starting with the fact that every monad gives raise to a Kleisli Category whose objects are the ones of the base category C and morphisms are of the form f? : b ! T a for each f : b ! a in C. Notice also that, nothing more than a design criteria, @arrow C a b implements a Coq type of maps de ned from b to a in the category C: Definition Kleisli_Category (C: Category) (T: Functor C C) (M: Monad C T): Category.
Proof. unshelve econstructor.
- exact (@obj C). - intros a b. exact (@arrow C (fobj T a) b).
...
Defined.
Once obtaining this category, we can then claim that there is a special adjunction, namely Kleisli adjunction, between the base category C and the Kleisli Category. We implement the candidate adjoint functors as in Equations (4) and (5). Below, we only show the way they map objects and arrows respectively.
Definition LA {C D: Category} (F: Functor C D) (G: Functor D C) (T , Compose_Functors F G) (M: Monad C T) (CT , (Kleisli_Category C T M)): Functor C CT.
Proof. unshelve econstructor; simpl.
- exact id. - intros a b f. exact (trans b o f).
...
Defined.
Definition RA {C D: Category} (F: Functor C D) (G: Functor D C) (T , Compose_Functors F G) (M: Monad C T) (CT , (Kleisli_Category C T M)): Functor CT C.
Proof. unshelve econstructor; simpl.
- exact (fobj T). - intros a b g. exact (trans b o fmap T g).
...
Defined.
Above three de nitions are implemented in the source Monads.v. We then prove that these candidate functors do actually form an adjunction:
Theorem mon_kladj: 8 {C D: Category} (F: Functor C D) (G: Functor D C) (T , Compose_Functors F G) (M: Monad C T) (FT , LA F G M) (GT , RA F G M), Adjunction FT GT.
Now, we can state Theorem 1.4 in Coq.
Notice that proving this statement, we only get the existence of a comparison functor L satisfying the given properties but not that it is unique. Unicity proof is actually the work in progress. Also, we have formalized the dual of this theorem again leaving the unicity proof of comparison functor aside. See Coq proofs of two theorems above and the dual of the comparison theorem in the source Adjunctions.v. 3
We have formalized in Coq the comparison theorem without proving the uniqueness of comparison functor L. This uniqueness (also for the dual case) is the next property in our queue to formalize. Once getting these done, we plan to continue with implementing in Coq the proof of Beck's theorem which is a variant of comparison theorem where CT being the Eilenberg-Moore category of algebras of the monad T. The theorem claims that the comparison functor L is now an isomorphism. 3.1
Acknowledgements This work has been supported by the Austrian Science Fund (FWF) grant P26201, the European Research Council (ERC) grant no. 714034 SMART. [Eki15]
Burak Ekici. Certi cations of programs with computational e ects (Certi cation de programmes avec des e ets calculatoires). PhD thesis, Grenoble Alpes University, France, December 2015. [Hen08] Christopher Henderson. Generalized abstract nonsense: Category theory and adjunctions. Technical report, University of Chicago, 2008. [TJ16]