{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:38Z","timestamp":1779836738167,"version":"3.53.1"},"reference-count":25,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2020,6,17]],"date-time":"2020-06-17T00:00:00Z","timestamp":1592352000000},"content-version":"unspecified","delay-in-days":168,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Consider two widely used definitions of equality. That of Leibniz: one value equals another if any predicate that holds of the first holds of the second. And that of Martin-L\u00f6f: the type identifying one value with another is occupied if the two values are identical. The former dates back several centuries, while the latter is widely used in proof systems such as Agda and Coq. Here we show that the two definitions are isomorphic: we can convert any proof of Leibniz equality to one of Martin-L\u00f6f identity and\n                    <jats:italic>vice versa<\/jats:italic>\n                    , and each conversion followed by the other is the identity. One direction of the isomorphism depends crucially on values of the type corresponding to Leibniz equality satisfying functional extensionality and Reynolds\u2019 notion of parametricity. The existence of the conversions is widely known (meaning that if one can prove one equality then one can prove the other), but that the two conversions form an isomorphism (internally) in the presence of parametricity and functional extensionality is, we believe, new. Our result is a special case of a more general relation that holds between inductive families and their Church encodings. Our proofs are given inside type theory, rather than meta-theoretically. Our paper is a literate Agda script.\n                  <\/jats:p>","DOI":"10.1017\/s0956796820000155","type":"journal-article","created":{"date-parts":[[2020,6,17]],"date-time":"2020-06-17T03:47:23Z","timestamp":1592365643000},"source":"Crossref","is-referenced-by-count":1,"title":["Leibniz equality is isomorphic to Martin-L\u00f6f identity, parametrically"],"prefix":"10.1017","volume":"30","author":[{"given":"ANDREAS","family":"ABEL","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3862-4073","authenticated-orcid":false,"given":"JESPER","family":"COCKX","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3862-6856","authenticated-orcid":false,"given":"DOMINIQUE","family":"DEVRIESE","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"AMIN","family":"TIMANY","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"PHILIP","family":"WADLER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2020,6,17]]},"reference":[{"key":"S0956796820000155_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.042"},{"key":"S0956796820000155_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"S0956796820000155_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628139"},{"key":"S0956796820000155_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018612"},{"key":"S0956796820000155_ref6","unstructured":"Cavallo, E. & Harper, R. 2019. Parametric Cubical Type Theory. arXiV:1901.00489."},{"key":"S0956796820000155_ref14","unstructured":"Hofmann, M. & Streicher, T. (1996) The groupoid interpretation of type theory. In Venice Festschrift. Oxford University Press, pp. 83\u2013111."},{"key":"S0956796820000155_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"S0956796820000155_ref10","unstructured":"Cohen, C. , Coquand, T. , Huber, S. & M\u00f6rtberg, A. (2016) Cubical Type Theory: A constructive interpretation of the univalence axiom. Arxiv e-prints."},{"key":"S0956796820000155_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"S0956796820000155_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951917"},{"key":"S0956796820000155_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535852"},{"key":"S0956796820000155_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.006"},{"key":"S0956796820000155_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863592"},{"key":"S0956796820000155_ref15","unstructured":"Leibniz, G. (1686) Discourse on metaphysics."},{"key":"S0956796820000155_ref11","unstructured":"Developers, Coq . (2017) Coq documentation."},{"key":"S0956796820000155_ref1","unstructured":"Altenkirch, T. , McBride, C. & Swierstra, W. (2007) Observational equality, Now! In Workshop on Programming Languages Meets Program Verification. ACM, pp. 57\u201368."},{"key":"S0956796820000155_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3110276"},{"key":"S0956796820000155_ref12","unstructured":"Coquand, T. (1992) Pattern matching with dependent types. In Types for Proofs and Programs. TYPES."},{"key":"S0956796820000155_ref23","volume-title":"Resizing Rules \u2013 Their Use and Semantic Justification","author":"Voevodsky","year":"2011"},{"key":"S0956796820000155_ref21","unstructured":"Streicher, T. (1993) Investigations into Intensional Type Theory. Habilitation thesis, Ludwig-Maximilians-University Munich."},{"key":"S0956796820000155_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000372"},{"key":"S0956796820000155_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0040259"},{"key":"S0956796820000155_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209119"},{"key":"S0956796820000155_ref20","unstructured":"Reynolds, J. C. (1983) Types, abstraction, and parametric polymorphism. In Information Processing, Mason, R. E. A. (ed), North Holland, pp. 513\u2013523."},{"key":"S0956796820000155_ref22","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Univalent Foundations Program","year":"2013"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796820000155","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:11Z","timestamp":1779834971000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796820000155\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"references-count":25,"alternative-id":["S0956796820000155"],"URL":"https:\/\/doi.org\/10.1017\/s0956796820000155","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"article-number":"e17"}}