Indexed Induction-Recursion

We give two finite axiomatizations of indexed inductive-recursive definitions in intuitionistic type theory. They extend our previous finite axiomatizations of inductive-recursive definitions of sets to indexed families of sets and encompass virtually all definitions of sets which have been used in intuitionistic type theory. The more restricted of the two axiomatization arises naturally by considering indexed inductive-recursive definitions as initial algebras in slice categories, whereas the other admits

• Type: Conference
• Year: 2001
• Where: DAGSTUHL
• Authors: Peter Dybjer, Anton Setzer
• Keywords: DAGSTUHL 2001, DAGSTUHL 2007, Finite Axiomatizations, Indexed Inductive-recursive Definitions, Intuitionistic Type Theory