From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4916 Path: news.gmane.org!not-for-mail From: Andrej Bauer Newsgroups: gmane.science.mathematics.categories Subject: Decidability of the theory of a monad Date: Wed, 3 Jun 2009 13:10:21 +0200 Message-ID: Reply-To: Andrej Bauer NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1244043203 13183 80.91.229.12 (3 Jun 2009 15:33:23 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 3 Jun 2009 15:33:23 +0000 (UTC) To: categories list Original-X-From: categories@mta.ca Wed Jun 03 17:33:19 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1MBsSp-0001Fj-BQ for gsmc-categories@m.gmane.org; Wed, 03 Jun 2009 17:33:15 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1MBrlu-0007A8-Lz for categories-list@mta.ca; Wed, 03 Jun 2009 11:48:54 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:4916 Archived-At: Consider the theory of a monad, i.e., the axioms are those of a category and a monad given as a triple: an operation T on objects, for each object A a morphism eta_A : A -> T A, and an operation lift_{A,B} which maps morphisms f : A -> T B to lift f : T A -> T B. Concretely, the axioms are (where lift f is written f* and composition is juxtaposition): id f = f f id = f (f g) h = f (g h) eta* = id f* eta = f (f* g)* = f* g* Presumably, the equational theory (with partial operations) of such a triple is decidable. Is this known? If we ignore the types and partiality, we can attempt to turn the above equations into a confluent terminating rewrite system using the Knuth-Bendix algorithm, but it gets stuck (on various orderings I tried). A more categorical way of asking the same question is: what is a concrete description of the free "monad on a category" (is this the same as "free monad" on "free category"?). With kind regards, Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]