Impredicative Observational Equality
summary
Extends observational TTobs with an impredicative universe of definitionally proof‑irrelevant types and implements transport via a type‑casting/observational equality mechanism; the resulting system CCobs proves decidability of conversion by refusing to normalize impredicative proofs and instead normalizing only the proof‑relevant fragment. Formal results include a normalization proof in plain Martin‑Löf type theory and canonicity; limitation: no elimination for the accessibility predicate, so some inductive impredicative eliminations are unsupported.
AI-written summary · about
chapters (7)
- 0:00Intro
- 0:37What is impredicativity?
- 1:25Impredicativity in Dependent Type Theory
- 5:41Difficulties with impredicativity
- 9:21Taming the devil with proof irrelevance
- 13:20Uniqueness of Identity Proofs
- 16:34Impredicative Observational Type Theory
related talks
26mObservational Equality: Now for Good
29mObserving Definitional Equality
14mAdequacy for Algebraic Effects Revisited
36mMcTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
52mType Theory and its Meaning Explanations
30mNormalisation for First-Class Universe Levels
24mA Formalization of Opaque Definitions for a Dependent Type Theory
53mIntroduction to Intuitionistic Type Theory