Chapter 7: Basic Metatheory for Type Theory
In this chapter we discuss lambda encodings of data, which are schemes for representing inductive (or coinductive) data as functions.