Abstract
Original language  English 

Qualification  PhD 
Awarding Institution 

Supervisors/Advisors 

Award date  22 Jan 2014 
Publication status  Published  2013 
Fingerprint
Keywords
 logic
 MartinLöf type theory
 inductiveinductive definitions
 type theory
Cite this
}
Inductiveinductive definitions. / Nordvall Forsberg, Fredrik.
2013.Research output: Thesis › Doctoral Thesis
TY  THES
T1  Inductiveinductive definitions
AU  Nordvall Forsberg, Fredrik
PY  2013
Y1  2013
N2  The principle of inductiveinductive definitions is a principle for defining data types in MartinLöf Type Theory. It allows the definition of a set A, simultaneously defined with a family B ∶ A → Set indexed over A. Such forms of definitions have been used by several authors in order to for example define the syntax of Type Theory in Type Theory itself. This thesis gives a theoretical justification for their use. We start by giving a finite axiomatisation of a type theory with inductiveinductive definitions in the style of Dybjer and Setzer’s axiomatisation of inductiverecursive definitions. We then give a categorical characterisation of inductiveinductive definitions as initial objects in a certain category. This is presented using a general framework for elimination rules based on the concept of a Category with Families. To show consistency of inductiveinductive definitions, a settheoretical model is constructed. Furthermore, we give a translation of our theory with a simplified form of the elimination rule into the already existing theory of indexed inductive definitions. This translation does notseem possible for the general elimination rule. Extensions to the theory are investigated, such as a combined theory of inductiveinductiverecursive definitions, more general forms of indexing and arbitrarily high (finite) towers of inductiveinductive definitions.Even so, not all uses of inductiveinductive definitions in the literature (in particular the syntax of Type Theory) are covered by the theories presented. Finally, two larger, novel case studies of the use of inductiveinductive definitions are presented: Conway’s Surreal numbers and a formalisation of positive inductiverecursive definitions.
AB  The principle of inductiveinductive definitions is a principle for defining data types in MartinLöf Type Theory. It allows the definition of a set A, simultaneously defined with a family B ∶ A → Set indexed over A. Such forms of definitions have been used by several authors in order to for example define the syntax of Type Theory in Type Theory itself. This thesis gives a theoretical justification for their use. We start by giving a finite axiomatisation of a type theory with inductiveinductive definitions in the style of Dybjer and Setzer’s axiomatisation of inductiverecursive definitions. We then give a categorical characterisation of inductiveinductive definitions as initial objects in a certain category. This is presented using a general framework for elimination rules based on the concept of a Category with Families. To show consistency of inductiveinductive definitions, a settheoretical model is constructed. Furthermore, we give a translation of our theory with a simplified form of the elimination rule into the already existing theory of indexed inductive definitions. This translation does notseem possible for the general elimination rule. Extensions to the theory are investigated, such as a combined theory of inductiveinductiverecursive definitions, more general forms of indexing and arbitrarily high (finite) towers of inductiveinductive definitions.Even so, not all uses of inductiveinductive definitions in the literature (in particular the syntax of Type Theory) are covered by the theories presented. Finally, two larger, novel case studies of the use of inductiveinductive definitions are presented: Conway’s Surreal numbers and a formalisation of positive inductiverecursive definitions.
KW  logic
KW  MartinLöf type theory
KW  inductiveinductive definitions
KW  type theory
M3  Doctoral Thesis
ER 