  This paper proposes a definition of recognizable transducers over monads and
comonads, which bridges two important ongoing efforts in the current research
on regularity. The first effort is the study of regular transductions, which
extends the notion of regularity from languages into word-to-word functions.
The other important effort is generalizing the notion of regular languages from
words to arbitrary monads, introduced in arXiv:1502.04898. In this paper, we
present a number of examples of transducer classes that fit the proposed
framework. In particular we show that our class generalizes the classes of
Mealy machines and rational transductions. We also present examples of
recognizable transducers for infinite words and a specific type of trees called
terms. The main result of this paper is a theorem, which states the class of
recognizable transductions is closed under composition, subject to some
coherence axioms between the structure of a monad and the structure of a
comonad. Due to its complexity, we formalize the proof of the theorem in Coq
Proof Assistant. In the proof, we introduce the concepts of a context and a
generalized wreath product for Eilenberg-Moore algebras, which could be
valuable tools for studying these algebras.
