Fredrik Nordvall Forsberg: Alternative coding systems for inductive-recursive definitions

Fredrik Nordvall Forsberg, University of Strathclyde

Abstract: 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.

This is joint work with Neil Ghani, Peter Hancock, Conor McBride and Stephan Spahn.