{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T20:52:14Z","timestamp":1770238334712,"version":"3.49.0"},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2003,3,20]],"date-time":"2003-03-20T00:00:00Z","timestamp":1048118400000},"content-version":"unspecified","delay-in-days":19,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2003,3]]},"abstract":"<jats:p>Formalising mathematics in dependent type theory often requires to represent sets as setoids, \ni.e. types with an explicit equality relation. This paper surveys some possible definitions of \nsetoids and assesses their suitability as a basis for developing mathematics. According to \nwhether the equality relation is required to be reflexive or not we have total or partial setoid, \nrespectively. There is only one definition of total setoid, but four different definitions of partial \nsetoid, depending on four different notions of setoid function. We prove that one approach \nto partial setoids in unsuitable, and that the other approaches can be divided in two classes \nof equivalence. One class contains definitions of partial setoids that are equivalent to total \nsetoids; the other class contains an inherently different definition, that has been useful in the \nmodeling of type systems. We also provide some elements of discussion on the merits of each \napproach from the viewpoint of formalizing mathematics. In particular, we exhibit a difficulty \nwith the common definition of subsetoids in the partial setoid approach.<\/jats:p>","DOI":"10.1017\/s0956796802004501","type":"journal-article","created":{"date-parts":[[2003,3,27]],"date-time":"2003-03-27T15:04:19Z","timestamp":1048777459000},"page":"261-293","source":"Crossref","is-referenced-by-count":63,"title":["Setoids in type theory"],"prefix":"10.1017","volume":"13","author":[{"given":"GILLES","family":"BARTHE","sequence":"first","affiliation":[]},{"given":"VENANZIO","family":"CAPRETTA","sequence":"additional","affiliation":[]},{"given":"OLIVIER","family":"PONS","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2003,3,20]]},"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796802004501","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,30]],"date-time":"2019-03-30T19:03:40Z","timestamp":1553972620000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796802004501\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":0,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,3]]}},"alternative-id":["S0956796802004501"],"URL":"https:\/\/doi.org\/10.1017\/s0956796802004501","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}