1    λ(f : Type → Type)
2  → λ(monad : ./../Monad/Type f)
3  → ./../Ran/lift
4    f
5    (./../Monad/extractFunctor f monad)
6    f
7    f
8    (./../Monad/terms.dhall f monad).join