Decidability of Conversion for Type Theory in Type Theory

Watch a 24-minute conference presentation from POPL 2018 exploring the formalization of a conversion checking algorithm for dependent type theory. Dive into how researchers from the University of Gothenburg, IMDEA Software Institute, and Chalmers University of Technology implemented and proved correct an algorithm for checking type equality in intensional type theory with one Russell-style universe, natural numbers, and η-equality for Π types. Learn how they utilized Agda to prove the algorithm's correctness through a Kripke logical relation and demonstrated both canonicity and completeness. Understand the significance of their approach working across different variants of intensional Martin-Löf Type Theory that support induction-recursion, including Extensional, Observational, and Homotopy Type Theory, without requiring uniqueness of identity proofs.