15

This chapter makes connections between convenient categories for models of the untyped lambda calculus and those of certain type structures. The main result that is needed later in Section 16.3 is the equivalence between the categories of natural type structures on the one hand and natural lambda structures on the other. This can be found in Section 15.2.

As a warm-up, a prototype result in this direction is Corollary 15.1.23, stating the equivalence between the category **MSL**^{U} of meet semi-lattices with universe, and the category **ALG*** _{a}* of algebraic lattices with additive morphisms that preserve compactness. The idea is that, by definition, in an algebraic lattice an element

Start Free Trial

No credit card required