Skip to Main content Skip to Navigation
Conference papers

Observational Equality: Now For Good

Abstract : Building on the recent extension of dependent type theory with a universe of definitionally proof-irrelevant types, we introduce TT obs , a new type theory based on the setoidal interpretation of dependent type theory. TT obs equips every type with an identity relation that satisfies function extensionality, propositional extensionality, and definitional uniqueness of identity proofs (UIP). Compared to other existing proposals to enrich dependent type theory with these principles, our theory features a notion of reduction that is normalizing and provides an algorithmic canonicity result, which we formally prove in Agda using the logical relation framework of Abel et al. Our paper thoroughly develops the meta-theoretical properties of TT obs , such as the decidability of the conversion and of the type checking, as well as consistency. We also explain how to extend our theory with quotient types, and we introduce a setoidal version of Swan's Id types that turn it into a proper extension of MLTT with inductive equality.
Complete list of metadata

https://hal.inria.fr/hal-03367052
Contributor : Nicolas Tabareau Connect in order to contact the contributor
Submitted on : Wednesday, October 20, 2021 - 11:44:36 AM
Last modification on : Wednesday, November 10, 2021 - 4:07:28 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03367052, version 2

Collections

Citation

Loïc Pujet, Nicolas Tabareau. Observational Equality: Now For Good. POPL, Jan 2022, Philadelphie, United States. ⟨hal-03367052v2⟩

Share

Metrics

Record views

66

Files downloads

91