Internal Parametricity Without an Interval

Explore a groundbreaking approach to internal parametricity in type theory through this 19-minute conference talk from POPL 2024. Delve into a novel extension of Martin-Löf type theory that achieves internal parametricity without relying on explicit higher-dimensional cubes or interval sorts. Discover how the presenters, Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, and Michael Shulman, introduce new type formers, term formers, and equations to create a simpler syntax where geometry emerges implicitly. Learn about the presheaf model over the BCH cube category, the span-based parametricity approach, and the gluing model that ensures external parametricity and canonicity. Gain insights into this theory's potential as a special case of modal type theory and its implications for demonstrating computational properties in higher observational type theory.

[POPL'24] Internal parametricity, without an interval