Canonicity for Indexed Inductive-Recursive Types
summary
Proves canonicity for Martin-Löf type theory with a countable universe hierarchy where every universe supports indexed inductive-recursive types. Method is two steps: construct IIR types from IR types plus basic formers so they obey Agda’s definitional computation rules, then prove canonicity for IR types by gluing along the global sections functor and encoding each IR canonicity predicate as a meta-level IIR type. Uses quotient inductive-inductive syntax and constructive gluing, yields a concrete evaluation/canonicity algorithm that succeeds. countable universe hierarchy gluing along global sections
AI-written summary · about
chapters (10)
- 0:00Introduction
- 4:32Inductive-recursive types
- 9:53Canonicity formalization
- 13:24Canonicity predicate
- 16:56Handling in proof
- 20:12Computational intuition
- 22:17Indexed induction recursion
- 23:20Summary of results
- 24:23Future work
- 25:48Q&A
related talks
22mA Calculus of Inductive Linear Constructions
40mHigher Inductive Types in Homotopy Type Theory
25mCubical Synthetic Homotopy Theory
53mIntroduction to Intuitionistic Type Theory
14mA Limited Case for Reification by Type Inference
13mA Simpler Encoding of Indexed Types
26mObservational Equality: Now for Good
19mThree Equivalent Ordinal Notation Systems in Cubical Agda