Una de las grandes ventajas de los lenguajes funcionales puros es que permiten ser razonados ecuacionalmente, de esta forma, se facilita la verificacion de su correccion. Pero esta pureza impide los efectos computacionales necesarios para que este tipo de programas tengan interaccion alguna, es por esto que las funciones monadicas, que se encargan de encapsular estos efectos y asi conservar la pureza, representan una estructura importante dentro de los lenguajes funcionales. Sin embargo, debido a que las monadas poseen una estructura imperativa, no se ha podido establecer un enfoque aceptado para razonar ecuacionalmente sobre estas. Por tanto, se pretende formalizar (desde un punto de vista computacional) en Agda la propuesta realizada por Gibbons y Hinze en [7] minimizando asi los errores en los pasos de cada una de las demostraciones. Asi pues, se presentan los conceptos basicos que permitan comprender como se razona sobre los programas y se muestra mediante un ejemplo la posibilidad de formalizar este razonamiento.