3 votes

Why does the CwF definition require a set of types under a context rather than a class of types?

There is nothing special about types with respect to sizing, compared to what we already have in ordinary categories. A small category has a set of objects, and for each pair of objects, a set of ...
user avatar
1 vote

What is the definition of a redex and what are they for in programming languages literature?

A redex is an expressions on which we can perform a computation step, such as: fst (a, b) is a redex, it computes to a ...
user avatar
  • 28.4k

Only top scored, non community-wiki answers of a minimum length are eligible