This talk is based on joint work (in progress) with Anton Setzer, Uppsala, on the syntax and semantics of large sets in Martin-Lof type theory. We give a new formulation of a very general class of universe operators introduced by so called simultaneous inductive-recursive definitions. We also show how to model such universe operators in classical set theory assuming the existence of certain large cardinals.

In this talk I want to give an introduction to this work. I will begin by discussing the syntax and semantics of recursive data types in strong functional programming (in the sense of David Turner). Then I show that when we generalize this to strong functional programming with dependent types, we are naturally led into the world of analogues of large cardinals. I will say something about the relationship between such "large" recursive data types and some notions of large cardinals in set theory (inaccessible cardinals, hyperinaccessible cardinals, and Mahlo cardinals).