{-
The currying isomorphism is defined for any closed monoidal (semigroupal?)
category (semigroupoid?), based on the – ⊗ X ⊣ Hom(X, –) odjunction.

**FIXME**: Because closed categories are self-enriched and `Isomorphism`
 currently has to be enriched by a category where the objects are types, this is
 currently restricted to categories where the objects are types.
-}
let kCat = ../../Cat/semigroupal

let object = Type

in  λ(cat : ./Kind kCat object) →
      ∀(a : object) →
      ∀(b : object) →
      ∀(c : object) →
        ../../../Isomorphism/Type
          object
          (../extractCategory kCat object object cat)
          { _1 = cat.arrow { _1 = cat.product { _1 = a, _2 = b }, _2 = c }
          , _2 = cat.arrow { _1 = a, _2 = cat.arrow { _1 = b, _2 = c } }
          }