--     let cat = ./../Category/Cat/semigroupal

-- in    λ(bObject : Kind)
--     → λ(cObject : Kind)
--     → λ(dObject : Kind)
--     → λ(bArrow : cat.arrow (cat.product dObject dObject) Type)
--     → λ(cArrow : cat.arrow (cat.product cObject cObject) Type)
--     → λ(dArrow : cat.arrow (cat.product dObject dObject) Type)
--     → λ(f : cat.arrow dObject cObject)
--     → λ(g : cat.arrow cObject dObject)
--     → λ(l : ./Type cObject dObject cArrow dArrow f g)
--     → λ(h : cat.arrow cObject bObject)
--     → λ(i : cat.arrow bObject cObject)
--     → λ(r : ./Type bObject cObject bArrow cArrow h i)
--     →   { unit =
--             l.leftAdjunct r.leftAdjunct
--         , counit :
--             r.rightAdjunct l.rightAdjunct
--         , leftAdjunct :
--               ∀(a : dObject)
--             → ∀(b : cObject)
--             → cArrow { _1 = f a, _2 = b }
--             → dArrow { _1 = a, _2 = g b }
--         , rightAdjunct :
--               ∀(a : dObject)
--             → ∀(b : cObject)
--             → dArrow { _1 = a, _2 = g b }
--             → cArrow { _1 = f a, _2 = b }
--         }
--       : ./../Type
--         bObject
--         dObject
--         bArrow
--         dArrow
--         (./Type dObject cObject bObject h f)
--         (./Type bObject cObject dObject g i)
<>