Sciweavers

DAGSTUHL
2001

Indexed Induction-Recursion

13 years 5 months ago
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
Peter Dybjer, Anton Setzer
Added 31 Oct 2010
Updated 31 Oct 2010
Type Conference
Year 2001
Where DAGSTUHL
Authors Peter Dybjer, Anton Setzer
Comments (0)