Document Open Access Logo

On Equality of Objects in Categories in Constructive Type Theory

Author Erik Palmgren

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2017.7.pdf
  • Filesize: 301 kB
  • 7 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • type theory
  • formalization
  • category theory
  • setoids

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

In this note we remark on the problem of equality of objects in categories formalized in Martin-Löf's constructive type theory. A standard notion of category in this system is E-category, where no such equality is specified. The main observation here is that there is no general extension of E-categories to categories with equality on objects, unless the principle Uniqueness of Identity Proofs (UIP) holds. We also introduce the notion of an H-category with equality on objects, which makes it easy to compare to the notion of univalent category proposed for Univalent Type Theory by Ahrens, Kapulkin and Shulman.

Cite As Get BibTex

Erik Palmgren. On Equality of Objects in Categories in Constructive Type Theory. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 7:1-7:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.TYPES.2017.7

Author Details

Erik Palmgren
  • Department of Mathematics, Stockholm University, Stockholm, Sweden

References

  1. Peter Aczel. Galois: a theory development project. Report for the 1993 Turin meeting on the Representation of Mathematics in Logical Frameworks, 1995. URL: http://www.cs.man.ac.uk/~petera/papers.html.
  2. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Math. Structures Comput. Sci., 25(5):1010-1039, 2015. Google Scholar
  3. Gilles Barthe, Venanzio Capretta, and Olivier Pons. Setoids in type theory. Journal of Functional Programming, 13:261-293, 2003. Google Scholar
  4. Errett Bishop. Foundations of constructive analysis. McGraw-Hill Book Co., New York-Toronto, Ont.-London, 1967. Google Scholar
  5. Saunders Mac Lane. Categories for the working mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, second edition, 1998. Google Scholar
  6. Erik Palmgren. Proof-relevance of families of setoids and identity in type theory. Arch. Math. Logic, 51(1-2):35-47, 2012. Google Scholar
  7. Erik Palmgren. Constructions of categories of setoids from proof-irrelevant families. Arch. Math. Logic, 56(1-2):51-66, 2017. Google Scholar
  8. Erik Palmgren and Olov Wilander. Constructing categories and setoids of setoids in type theory. Log. Methods Comput. Sci., 10(3):3:25, 14, 2014. Google Scholar
  9. The Univalent Foundations Program. Homotopy type theory - univalent foundations of mathematics. The Univalent Foundations Program, Princeton, NJ; Institute for Advanced Study (IAS), Princeton, NJ, 2013. Google Scholar
  10. Olov Wilander. Constructing a small category of setoids. Math. Structures Comput. Sci., 22(1):103-121, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact