On Equality of Objects in Categories in Constructive Type Theory

Palmgren, Erik

doi:10.4230/LIPIcs.TYPES.2017.7

File

LIPIcs.TYPES.2017.7.pdf

Filesize: 301 kB
7 pages

Document Identifiers

DOI: 10.4230/LIPIcs.TYPES.2017.7
URN: urn:nbn:de:0030-drops-100553

Author Details

Erik Palmgren

Department of Mathematics, Stockholm University, Stockholm, Sweden

Cite AsGet 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

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.

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

References

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.
Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Math. Structures Comput. Sci., 25(5):1010-1039, 2015.
Gilles Barthe, Venanzio Capretta, and Olivier Pons. Setoids in type theory. Journal of Functional Programming, 13:261-293, 2003.
Errett Bishop. Foundations of constructive analysis. McGraw-Hill Book Co., New York-Toronto, Ont.-London, 1967.
Saunders Mac Lane. Categories for the working mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, second edition, 1998.
Erik Palmgren. Proof-relevance of families of setoids and identity in type theory. Arch. Math. Logic, 51(1-2):35-47, 2012.
Erik Palmgren. Constructions of categories of setoids from proof-irrelevant families. Arch. Math. Logic, 56(1-2):51-66, 2017.
Erik Palmgren and Olov Wilander. Constructing categories and setoids of setoids in type theory. Log. Methods Comput. Sci., 10(3):3:25, 14, 2014.
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.
Olov Wilander. Constructing a small category of setoids. Math. Structures Comput. Sci., 22(1):103-121, 2012.