Preprint available: On equality of objects in categories in constructive type theory

[Erik Palmgren]

Here is a new note that might be of interest to the readers of the list.
Whether to impose equality on objects in categories, and what kind, is
an issue that becomes pressing in the formalization of models of
Martin-Löf type theory inside the theory itself.



On equality of objects in categories in constructive type theory

Erik Palmgren

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, a variant of 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.

Link to preprint:

http://staff.math.su.se/palmgren/eobcat.pdf