{-|

**TODO**: This would be `./../Group/Type … (./../Category/Monoidal/Profunctor
object morphism)`, but `Category` isn’t defined via `Monoid`, so we prefer
compatibility with that.
-}
let kCat = ../Category/Cat/semigroupal

let vObject = Type

in  λ(object : Kind) →
    λ(v : ../Category/Monoidal/Kind kCat Type vObject) →
    λ(cat : ../Category/Kind kCat vObject object) →
        { inverse :
            ∀(a : kCat.product object object) →
            cat.arrow a →
              cat.arrow { _1 = a._2, _2 = a._1 }
        }
      ⩓ ../Category/Type object v cat