let kCat = ../Category/Cat/semigroupal

let vObject = Type

let v =
      ../Category/Monoidal/Cartesian/extractMonoidal
        kCat
        Type
        vObject
        ../Category/Set/monoidal/cartesian

let object = Type

let cat =
      ../Category/Monoidal/Cartesian/extractCategory
        kCat
        vObject
        object
        ../Category/Set/monoidal/cartesian

in  λ(category : ../Category/Type object v cat) →
      let Codensity = ./Type object cat

      in  λ(m : kCat.arrow object object) →
              { unit =
                  λ(a : object) →
                  λ(x : a) →
                  λ(b : object) →
                  λ(k : cat.arrow { _1 = a, _2 = m b }) →
                    k x
              , product =
                  λ(a : object) →
                  λ(codensity : Codensity m (Codensity m a)) →
                  λ(c : object) →
                  λ(l : cat.arrow { _1 = a, _2 = m c }) →
                    codensity
                      c
                      ( λ(x : Codensity m a) →
                          category.unit (Codensity m a) x c l
                      )
              }
            : ../Monad/Type object cat (Codensity m)