Variations on inductive-recursive definitions

Fredrik Nordvall Forsberg, University of Strathclyde. Part of the proofs, constructions and computations seminar series.

Inductive-recursive definitions allows the simultaneous construction of a family (U : Set, T : U -> D) where U : Set is inductively defined, and the function T : U -> D is recursively defined for some (possibly large) type D. The prototypical example of an inductive-recursive definition is Martin-Löf\'s universe a la Tarski. Dybjer and Setzer gave an axiomatisation of inductive-recursive definitions by exhibiting them as initial algebras of certain functors between families Fam D -> Fam E. The question of composition of DS-definable functors arises naturally: given two DS-definable functors F : Fam C -> Fam D and G : Fam D -> Fam E, is their composition G . F : Fam C -> Fam E DS-definable? Perhaps surprisingly, the answer seems to be no. However, Dybjer and Setzer's axiomatisation is not the only possible one, and I will present two alternatives: first an axiomatisation of "uniform" definitions, which is a subsystem of Dybjer-Setzer's, and secondly a supersystem with a dependent product constructor added. Both of these systems are closed under composition.

Fredrik Nordvall Forsberg, University of Strathclyde