An Effectful Way to Eliminate Addiction to Dependence

We define a syntactic monadic translation of type theory, called the weaning translation, that allows for a large range of effects in
dependent type theory, such as exceptions, non-termination, non-determinism or writing operation. Through the light of a
call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially,
the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of
the Calculus of Inductive Constructions with a restricted version of dependent elimination, dubbed Baclofen Type Theory, which we conjecture
is the proper generic way to mix effects and dependence. This provides the first effectful version of CIC, which can be implemented as a Coq plugin.