×

Category theoretic structure of setoids. (English) Zbl 1418.18006

Summary: A setoid is a set together with a constructive representation of an equivalence relation on it. Here, we give category theoretic support to the notion. We first define a category \(\mathsf{Setoid}\) and prove it is Cartesian closed with coproducts. We then enrich it in the Cartesian closed category \(\mathsf{Equiv}\) of sets and classical equivalence relations, extend the above results, and prove that \(\mathsf{Setoid}\) as an \(\mathsf{Equiv}\)-enriched category has a relaxed form of equalisers. We then recall the definition of \(\mathcal E\)-category, generalising that of \(\mathsf{Equiv}\)-enriched category, and show that \(\mathsf{Setoid}\) as an \(\mathcal E\)-category has a relaxed form of coequalisers. In doing all this, we carefully compare our category theoretic constructs with Agda code for type-theoretic constructs on setoids.

MSC:

18D20 Enriched categories (over closed or monoidal categories)
03E70 Nonclassical and second-order set theories
18A35 Categories admitting limits (complete categories), functors preserving limits, completions
18B05 Categories of sets, characterizations

Software:

Agda
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bishop, E., Foundations of Constructive Analysis (1967), McGraw-Hill · Zbl 0183.01503
[2] (2012)
[3] (2012)
[4] (2012)
[5] Kelly, G., Elementary observations on 2-categorical limits, Bull. Aust. Math. Soc., 39, 301-317 (1989) · Zbl 0657.18004
[6] Aczel, P., Galois: a theory development project (1993), report for the 1993 Turin meeting on the Representation of Mathematics in Logical Frameworks
[7] Čubrić, D.; Dybjer, P.; Scott, P. J., Normalization and the Yoneda embedding, Math. Structures Comput. Sci., 8, 2, 153-192 (1998) · Zbl 0918.03012
[8] Kinoshita, Y., A bicategorical analysis of E-categories, Math. Jpn., 47, 1, 157-169 (1998) · Zbl 0923.18001
[9] Wilander, K. O., An e-bicategory of e-categories: exemplifying a typetheoretic approach to bicategories (2005), Uppsala University, Department of Mathematics, Tech. Rep. 2005:48
[10] Wilander, K. O., Setoids and universes, Math. Structures Comput. Sci., 20, 563-576 (2010) · Zbl 1204.03060
[11] Wilander, K. O., On constructive sets and partial structures (2011), Uppsala University, Department of Mathematics, Ph.D. thesis
[12] Wilander, K. O., Constructing a small category of setoids, Math. Structures Comput. Sci., 22, 103-121 (2012) · Zbl 1261.03176
[13] Carboni, A.; Magno, R. C., The free exact category on a left exact one, J. Austral. Math. Soc., 33, A, 295-301 (1982) · Zbl 0504.18005
[14] Carboni, A., Some free constructions in realizability and proof theory, J. Pure Appl. Algebra, 103, 117-148 (1995) · Zbl 0839.18002
[15] Carboni, A.; Rosolini, G., Locally Cartesian closed exact completions, J. Pure Appl. Algebra, 154, 103-116 (2000) · Zbl 0962.18001
[16] Maietti, M. E.; Rosolini, G., Quotient completion for the foundation of constructive mathematics, Cornell University, 2012
[17] Maietti, M. E.; Rosolini, G., Elementary quotient completion, Cornell University, 2012
[18] Maietti, M. E.; Rosolini, G., Unifying exact completions, Cornell University, 2012
[19] Kelly, G. M., Basic Concepts of Enriched Category Theory, Reprints in Theory and Aplications of Categories, vol. 10 (2005) · Zbl 1086.18001
[20] Bénabou, J., Introduction to bicategories, (Reports of the Midwest Category Seminar. Reports of the Midwest Category Seminar, Lecture Notes in Math., vol. 47 (1967), Springer: Springer Berlin, Heidelberg), 1-77 · Zbl 1375.18001
[21] Street, R., Fibrations in bicategories, Cah. Topol. Géom. Différ. Catég., 21, 2, 111-160 (1980) · Zbl 0436.18005
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.