Can we formalise type theory intrinsically without any compromise? A case study in(…)

on YouTube ↗23m

" summary

An intrinsic syntax for dependent type theory is encoded in Cubical Agda using quotient inductive-inductive-recursive types to define the initial natural model without postulates or transports; basic features, a universe, and normalization-by-evaluation for the substitution calculus all compute and work. However pervasive transport hell reappears for logical predicates, pi-types, and more sophisticated metatheory, and strictification only partially helps, so the project succeeds for core constructions but not yet without compromise.

AI-written summary · about

" chapters (18)

1. 0:00Introduction
2. 0:45Motivation for formalizing type theory
3. 2:14Dependent types and circular dependencies
4. 3:38Historical approaches to syntax
5. 5:04Quotient inductive types breakthrough
6. 6:50Cubical Agda implementation issues
7. 8:54Transport problems and Henry Ford principle
8. 10:37Natural models and new data type
9. 12:43Extending model with type features
10. 13:44Initiality property and recursion
11. 15:52Constructing standard and term models
12. 16:34Normalization by evaluation
13. 17:16Logical predicates model attempt
14. 18:38Limitations of strictification
15. 18:58Summary and open questions
16. 20:03Q&A: Contexts and universes
17. 21:07Q&A: Determinacy and naturality
18. 22:09Q&A: Indexed vs unindexed syntax