Completed
Examples of inductive-recursive definitions in type theory
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Peter Dybjer - Intuitionistic Type Theory
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 Plan of lectures on Intuitionistic Type Theory
- 3 The LF version of Intuitionistic Type Theory 1986
- 4 Rules for natural numbers in Agda
- 5 Rules for the identity set in Agda
- 6 Intuitionistic Type Theory 1986 have decidable judgments
- 7 Intuitionistic Type Theory as a Theory of Inductive Definitions
- 8 Iterated inductive definitions in predicate logic
- 9 Inductive families
- 10 Generalized Inductive definitions
- 11 Examples of inductive-recursive definitions in type theory
- 12 General schema for inductive-recursive types
- 13 Finite axiomatization of Inductive types
- 14 Some codes
- 15 Finite axiomatization of Inductive-recursive types
- 16 Code for universe closed under
- 17 Three views of Intuitionistic Type Theory
