Hostname: page-component-8448b6f56d-gtxcr Total loading time: 0 Render date: 2024-04-19T13:39:57.953Z Has data issue: false hasContentIssue false

Setoids in type theory

Published online by Cambridge University Press:  20 March 2003

GILLES BARTHE
Affiliation:
INRIA Sophia-Antipolis, 2004 Route des Lucioles, BP 93, 06902 Sophia Antipolis Cedex, France (e-mail: Gilles.Barthe@inria.fr)
VENANZIO CAPRETTA
Affiliation:
INRIA Sophia-Antipolis, 2004 Route des Lucioles, BP 93, 06902 Sophia Antipolis Cedex, France (e-mail: Venanzio.Capretta@inria.fr)
OLIVIER PONS
Affiliation:
CNAM, France (e-mail: pons@cnam.fr)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Formalising mathematics in dependent type theory often requires to represent sets as setoids, i.e. types with an explicit equality relation. This paper surveys some possible definitions of setoids and assesses their suitability as a basis for developing mathematics. According to whether the equality relation is required to be reflexive or not we have total or partial setoid, respectively. There is only one definition of total setoid, but four different definitions of partial setoid, depending on four different notions of setoid function. We prove that one approach to partial setoids in unsuitable, and that the other approaches can be divided in two classes of equivalence. One class contains definitions of partial setoids that are equivalent to total setoids; the other class contains an inherently different definition, that has been useful in the modeling of type systems. We also provide some elements of discussion on the merits of each approach from the viewpoint of formalizing mathematics. In particular, we exhibit a difficulty with the common definition of subsetoids in the partial setoid approach.

Type
Special Issue on Logical frameworks and metalanguages
Copyright
© 2003 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.