Hi,

Simply-typed lambda calculus can be modelled by any Cartesian closed
category where arrow types are modelled by exponentials, product types are
modelled by products, the single-element type is modelled by terminal
object, and beta-eta equivalence classes of terms-in-context are modelled
by morphisms.

Now suppose we have a complete Cartesian closed category. Which kind of
type would be moldelled by limits? In other words, how can I understand
the notion of limit from a computer scientist point of view? Same question
for colimits.

Thanks.

David