{-|

**FIXME**: This should use `./../Monoid/Type …
(./../Category/Monoidal/Profunctor object morphism)`, but the unit in that
monoidal category definition isn’t correct (or, if it is, I can’t figure out how
to use it). So instead, we just build the `Semigroup`, and then write a custom
unit. But this means we’re not structurally a `Monoid`.
-}
let kCat = ./Cat/semigroupal

let vObject = Type

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