Set-based mappings

Any mapping , where X and Y are classes, that satisfies the following property: is called set-based mapping. We may consider recursive types of the form: by considering set-based mapping where . However, we will not spend our time on doing that in the full generality. Later in the today's class, we will restrict the set of admissible set-based mappings to the monotone ones. It will help us to add function type to primitive recursive types and to introduce something which is really miraculous - co-inductive types.

Now, we will use the example of natural numbers defined as a primitive recursive type to help us understand how elements of any given type are obtained. Consider (1 is our informal notation for type ). Clearly, there is one element we can get right now: - we can think of it as of zero. Now, we can informally say that in order to obtain more elements of natural numbers it is sufficient to apply inr to what we already have. If one thinks of inr as succ, it is clear that we obtained natural numbers by defining them as one of primitive recursive types. However, our approach is general - we can define many types of types, and we also have a general rule of induction over them, together with primitive recursion.

In order to define more formally the type of an element, we say that iff This basically captures the notion of unfolding the primitive recursive type definition. Similarly, we can define equality: iff It is worth noting that equality is decidable in primitive recursive types (to prove this statement is given as one of the problems in Problem Set 3).