--   λ(object : Kind)
-- → λ(arrow : object → object → Type)
-- → λ(semigroupoid : ./../Semigroupoid/Type object arrow)
-- → λ(w : object → object)
-- →     let costarArrow = ./Type object arrow w

--   in    λ(comonad : ./../Comonad/Type object arrow w)
--       →     let extend =
--                   ( ./../Comonad/impliedCostarfunctor
--                     object
--                     arrow
--                     semigroupoid
--                     w
--                     comonad
--                   ).map

--         in    { unit =
--                   comonad.unit
--               , compose =
--                     λ(a : object)
--                   → λ(b : object)
--                   → λ(c : object)
--                   → λ(g : costarArrow b c)
--                   → λ(f : costarArrow a b)
--                   → semigroupoid.compose (w a) (w b) c g (extend a b f)
--               }
--             : ./../Category/Type object costarArrow
<>