{-|

**TODO**: This currently forces 𝒱 = 𝐒𝐞𝐭, because of the Hom instance. It would
be good to abstract that via composition with some symmetric category, like
`category.product (hom.map a b) flip`.
-}
let kCat = ../Cat/semigroupal

let vObject = Type

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

in  λ(object : Kind) →
    λ(cat : ../Kind kCat vObject object) →
    λ(category : ../Type object v cat) →
      let Op = ./Kind vObject object cat

      in    { unit = category.unit
            , product =
                λ(a : { _1 : object, _2 : object }) →
                λ ( p
                  : ∀(r : Type) →
                    ( ∀(z : object) →
                      Op.arrow { _1 = z, _2 = a._2 } →
                      Op.arrow { _1 = a._1, _2 = z } →
                        r
                    ) →
                      r
                  ) →
                  category.product
                    { _1 = a._2, _2 = a._1 }
                    ( λ(r : Type) →
                      λ ( arrowsOut
                        : ∀(z : object) →
                          cat.arrow { _1 = z, _2 = a._1 } →
                          cat.arrow { _1 = a._2, _2 = z } →
                            r
                        ) →
                        p
                          r
                          ( λ(z : object) →
                            λ(f : Op.arrow { _1 = z, _2 = a._2 }) →
                            λ(g : Op.arrow { _1 = a._1, _2 = z }) →
                              arrowsOut z g f
                          )
                    )
            , hom.map
              =
                λ(a : { _1 : object, _2 : object }) →
                λ(b : { _1 : object, _2 : object }) →
                λ ( f
                  : { _1 : cat.arrow { _1 = a._1, _2 = b._1 }
                    , _2 : cat.arrow { _1 = b._2, _2 = a._2 }
                    }
                  ) →
                  category.hom.map
                    { _1 = a._2, _2 = a._1 }
                    { _1 = b._2, _2 = b._1 }
                    { _1 = f._2, _2 = f._1 }
            }
          : ../Type object v Op