Modules over monads and typoids

Abstract: We define a notion of module over a monad and use it to propose a new definition (or semantics) for abstract syntax (with binding constructions). Using our notion of module, we build a category of exponential monads, which can be understood as the category of lambda-calculi, and prove that it has an initial object (the pure untyped lambda-calculus). We explore how these results could be formalized in the proof assistant Coq. In this context we introduce the category of setoids. We equip this category with a model structure where cofibrant-fibrant objects are sets. In this way, homotopy theory provides a unified approach to several categories of variants of sets.