Peter Dybjer - Intuitionistic Type Theory

Explore the third lecture in a series on Intuitionistic Type Theory, delivered by Peter Dybjer as part of the Hausdorff Trimester Program: Types, Sets and Constructions. Delve into advanced topics such as the LF version of Intuitionistic Type Theory, rules for natural numbers and identity sets in Agda, and the concept of Intuitionistic Type Theory as a theory of inductive definitions. Examine iterated inductive definitions in predicate logic, inductive families, and generalized inductive definitions. Discover examples of inductive-recursive definitions in type theory and learn about the general schema for inductive-recursive types. Explore the finite axiomatization of inductive and inductive-recursive types, along with codes for universes closed under certain operations. Gain insights into three different perspectives on Intuitionistic Type Theory in this comprehensive 70-minute lecture.

Intro
Plan of lectures on Intuitionistic Type Theory
The LF version of Intuitionistic Type Theory 1986
Rules for natural numbers in Agda
Rules for the identity set in Agda
Intuitionistic Type Theory 1986 have decidable judgments
Intuitionistic Type Theory as a Theory of Inductive Definitions
Iterated inductive definitions in predicate logic
Inductive families
Generalized Inductive definitions
Examples of inductive-recursive definitions in type theory
General schema for inductive-recursive types
Finite axiomatization of Inductive types
Some codes
Finite axiomatization of Inductive-recursive types
Code for universe closed under
Three views of Intuitionistic Type Theory