{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T07:38:10Z","timestamp":1790840290790,"version":"4.1.0"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>Building on the recent extension of dependent type theory with a universe of definitionally proof-irrelevant types, we introduce TTobs, a new type theory based on the setoidal interpretation of dependent type theory. TTobs 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 TTobs, 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.<\/jats:p>","DOI":"10.1145\/3498693","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T12:03:12Z","timestamp":1641988992000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Observational equality: now for good"],"prefix":"10.1145","volume":"6","author":[{"given":"Lo\u00efc","family":"Pujet","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3366-2273","authenticated-orcid":false,"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(2:14)2020"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71989-X"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782636"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33636-3_7"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2016.21"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434341"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_2_2_14_1","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de Doctorat d\u2019\u00c9tat Universit\u00e9 de Paris VII.  Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de Doctorat d\u2019\u00c9tat Universit\u00e9 de Paris VII."},{"key":"e_1_2_2_15_1","unstructured":"Martin Hofmann. 1993. Non Strictly Positive Datatypes in System F. Email on the Types mailing list. http:\/\/www.seas.upenn.edu\/~sweirich\/types\/archive\/1993\/msg00027.html  Martin Hofmann. 1993. Non Strictly Positive Datatypes in System F. Email on the Types mailing list. http:\/\/www.seas.upenn.edu\/~sweirich\/types\/archive\/1993\/msg00027.html"},{"key":"e_1_2_2_17_1","unstructured":"Chris Kapulkin and Peter LeFanu Lumsdaine. 2018. The simplicial model of Univalent Foundations (after Voevodsky). arxiv:1211.2851.  Chris Kapulkin and Peter LeFanu Lumsdaine. 2018. The simplicial model of Univalent Foundations (after Voevodsky). arxiv:1211.2851."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.24"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.31"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.4115\/jla.2016.8.1"},{"key":"e_1_2_2_22_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Foundations Program The Univalent","unstructured":"The Univalent Foundations Program . 2013. Homotopy Type Theory: Univalent Foundations of Mathematics . Institute for Advanced Study . https:\/\/homotopytypetheory.org\/book\/ The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. https:\/\/homotopytypetheory.org\/book\/"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_2_2_24_1","unstructured":"Vladimir Voevodsky. 2013. A simple type system with two identity types. https:\/\/ncatlab.org\/homotopytypetheory\/files\/HTS.pdf  Vladimir Voevodsky. 2013. A simple type system with two identity types. https:\/\/ncatlab.org\/homotopytypetheory\/files\/HTS.pdf"},{"key":"e_1_2_2_25_1","first-page":"1181","article-title":"A C-system defined by a universe category","volume":"30","author":"Voevodsky Vladimir","year":"2015","unstructured":"Vladimir Voevodsky . 2015 . A C-system defined by a universe category . Theory Appl. Categ. , 30 (2015), No. 37, 1181 \u2013 1215 . issn:1201-561X http:\/\/www.tac.mta.ca\/tac\/volumes\/30\/37\/30-37abs.html Vladimir Voevodsky. 2015. A C-system defined by a universe category. Theory Appl. Categ., 30 (2015), No. 37, 1181\u2013 1215. issn:1201-561X http:\/\/www.tac.mta.ca\/tac\/volumes\/30\/37\/30-37abs.html","journal-title":"Theory Appl. Categ."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498693","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498693","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T15:30:28Z","timestamp":1750174228000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498693"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":23,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498693"],"URL":"https:\/\/doi.org\/10.1145\/3498693","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}