let kCat = ../Cat/semigroupal

let vObject = Type

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

      in    { leftIdentity :
                ∀(a : object) →
                  Isomorphism
                    { _1 = cat.product { _1 = cat.unit, _2 = a }, _2 = a }
            , rightIdentity :
                ∀(a : object) →
                  Isomorphism
                    { _1 = cat.product { _1 = a, _2 = cat.unit }, _2 = a }
            }
          ⩓ ../Semigroupal/Type
              object
              v
              (./extractSemigroupal kCat vObject object cat)