-- {-|
-- `bool` is some sort of `Const` functor in the correct category that can be
-- converted to a `Bool`.
-- -}
--   λ(object : Kind)
-- → λ(cat : ./../Category/Monoidal/Kind kCat object)
-- → λ(bool : object)
-- → λ(a : object)
-- → { eq : cat.arrow { _1 = cat.product { _1 = a, _2 = a }, _2 = bool } }
λ(a : Type) → { eq : a → a → Bool }