let cat = ../../Category/Cat/semigroupal

let vObject = Type

in    { constraint =
          λ(t : Type) →
            ../../Functor/Constant/Type Type Type { _1 = {}, _2 = t }
      , arrow = λ(a : { _1 : Type, _2 : Type }) → a._1 → a._2
      , additive =
        { unit = <>
        , product =
            λ(a : { _1 : Type, _2 : Type }) → < Left : a._1 | Right : a._2 >
        }
      , multiplicative =
        { unit = {}
        , product = λ(a : { _1 : Type, _2 : Type }) → { _1 : a._1, _2 : a._2 }
        }
      }
    : ../Rig/Kind cat vObject Type