Abstract

In order to represent, compute and reason with advanced data types like lists with a fixed length, finite sets or well scoped λ-terms one must go beyond the traditional treatment of data types as being inductive types and, instead, consider them as inductive families, or more precisely Strictly Positive Families (SPFs). We have previously shown that the grammar of strictly positive types (SPT) can be given as an inductively defined family. In the present paper we go one step further an show that the universe of SPFs can be encoded as an SPF. We show that SPFs can be used to represent and compute with a variety of advanced data types and that generic programs can be naturally written over the universe of SPFs.