let kCat = ../../Category/Cat/semigroupal

let base = ../../Category/Monoidal/extractCategory kCat

let vObject = Type

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

let Set =
      ../../Category/Rig/extractAdditive
        kCat
        vObject
        Type
        ../../Category/Set/rig

let cat = base vObject Type Set

in  λ(m : Type → Type) →
    λ ( functor
      : ../../Functor/Endo/Type vObject Type (base Type vObject v) cat m
      ) →
        { map =
            λ(a : { _1 : Type, _2 : Type }) →
            λ(b : { _1 : Type, _2 : Type }) →
            λ(f : { _1 : a._1 → m b._1, _2 : a._2 → m b._2 }) →
            λ(e : Set.product a) →
              let E = Set.product b

              in  merge
                    { Left =
                        λ(x : a._1) →
                          functor.map b._1 (Set.product b) E.Left (f._1 x)
                    , Right =
                        λ(x : a._2) →
                          functor.map b._2 (Set.product b) E.Right (f._2 x)
                    }
                    e
        }
      : ../../Functor/Pair/Type
          vObject
          Type
          v
          (../../Category/Kleisli/category vObject Type cat m)
          Set.product