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

[Erik Palmgren <palm...@math.su.se>]

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