Positive Inductive-Recursive Definitions

A new theory of data types which allows for the definition of types asinitial algebras of certain functors Fam(C) -> Fam(C) is presented. Thistheory, which we call positive inductive-recursive definitions, is ageneralisation of Dybjer and Setzer's theory of inductive-recursive definitionswithin which C had to be discrete -- our work can therefore be seen as liftingthis restriction. This is a substantial endeavour as we need to not onlyintroduce a type of codes for such data types (as in Dybjer and Setzer's work),but also a type of morphisms between such codes (which was not needed in Dybjerand Setzer's development). We show how these codes are interpreted as functorson Fam(C) and how these morphisms of codes are interpreted as naturaltransformations between such functors. We then give an application of positiveinductive-recursive definitions to the theory of nested data types and we giveconcrete examples of recursive functions defined on universes by using theirelimination principle. Finally we justify the existence of positiveinductive-recursive definitions by adapting Dybjer and Setzer's set-theoreticmodel to our setting.Comment: 21 page