In the lectures prior to this one we developed the concept of inductive types based upon recursive definitions. This study culminated with the recursion-induction principle, and the concept of unwinding the type definition to construct elements.
The following set of notes attempt to explain inductive types in terms of set theory and inductively defined sets. The notes shall begin with an account of monotone operators, and how any inductively defined type can be expressed in terms of a monotone operator. The remainder of the notes will focus on finding the least fixed point of the sequence of sets defined by a monotone operator.