Observational Equality: Now for Good
summary
TTobs extends MLTT with a proof-irrelevant universe and an observational equality that satisfies function and propositional extensionality plus UIP while preserving normalization, canonicity and decidable conversion. The development includes a primitive cast operation, an extra constructor for indexed inductives to make casts eliminable, and quotient and squash constructions. Metatheory is machine-checked in Agda via Abel et al.’s logical-relations framework, a model gives consistency, and an Agda implementation (rewrite rules) exists with a planned Coq-kernel option.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 0:12Martin Luther
- 1:10Canonicity
- 2:12Workarounds
- 4:36Titty of Ttops
- 7:29Proof Relevant Layers
- 8:43Indexed and Active Types
- 10:21Extensionality
- 11:29Question Types
- 12:41Meta Theory
- 13:26Consistency
- 14:33normalization canonicity decidability
- 15:30pros and cons
- 17:11Semantics
- 18:45Implementation
- 19:41Questions
related talks
23mImpredicative Observational Equality
29mObserving Definitional Equality
14mAdequacy for Algebraic Effects Revisited
30mNormalisation for First-Class Universe Levels
53mIntroduction to Intuitionistic Type Theory
29mMechanized monadic equational reasoning for ML references
52mType Theory and its Meaning Explanations
24mAn Order-Theoretic Analysis of Universe Polymorphism