Abstract
When formalizing mathematics in constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids (types with explicit equivalence relations). In this note we consider two categories of setoids with equality on objects and show, within intensional Martin-Löf type theory, that they are isomorphic. Both categories are constructed from a fixed proof-irrelevant family F of setoids. The objects of the categories form the index setoid I of the family, whereas the definition of arrows differs. The first category has for arrows triples \((a,b,f:F(a)\,\rightarrow \,F(b))\) where f is an extensional function. Two such arrows are identified if appropriate composition with transportation maps (given by F) makes them equal. In the second category the arrows are triples \((a,b,R \hookrightarrow \Sigma (I,F)^2)\) where R is a total functional relation between the subobjects \(F(a), F(b) \hookrightarrow \Sigma (I,F)\) of the setoid sum of the family. This category is simpler to use as the transportation maps disappear. Moreover we also show that the full image of a category along an E-functor into an E-category is a category.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Altenkirch, T.: Extensional equality in intensional type theory. In: 14th Symposium on Logic in Computer Science, pp. 412–421. IEEE Press, Piscataway (1999)
Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13, 261–293 (2003)
Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill, New York (1967)
Hofmann, M.: Extensional Concepts in Intensional Type Theory. Springer, Berlin (1997)
Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: Sambin, G., Smith, J. (eds.) Twenty-five years of constructive type theory (Venice, 1995), Oxford Logic Guides, vol. 36, pp. 83–111. Oxford University Press, New York (1998)
Maietti, M.E., Rosolini, G.: Quotient completion for the foundation of constructive mathematics. Logica Universalis 7, 371–402 (2013)
Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf Type Theory. Oxford University Press, Oxford (1990)
Palmgren, E.: Proof-relevance of families of setoids and identity in type theory. Arch. Math. Log. 51, 35–47 (2012)
Palmgren, E., Wilander, O.: Constructing categories and setoids of setoids in type theory. Log. Methods Comput. Sci. 10(3), paper 25 (2014)
Wilander, O.: Constructing a small category of setoids. Math. Struct. Comput. Sci. 22, 103–121 (2012)
Author information
Authors and Affiliations
Corresponding author
Additional information
Title of earlier version (April 21, 2013): Yet another category of setoids with equality on objects.
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Palmgren, E. Constructions of categories of setoids from proof-irrelevant families. Arch. Math. Logic 56, 51–66 (2017). https://doi.org/10.1007/s00153-016-0514-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00153-016-0514-7