On equality of objects in categories in constructive type theory

TL;DR

This paper explores the conditions under which categories in constructive type theory can have equality on objects, highlighting the role of the UIP principle and introducing H-categories as a variant.

Contribution

It demonstrates that extending E-categories to categories with object equality requires UIP and introduces H-categories to compare with univalent categories.

Findings

No general extension of E-categories with equality without UIP

H-categories facilitate comparison with univalent categories

Highlights limitations of equality in categories in constructive type theory

Abstract

In this note we remark on the problem of equality of objects in categories formalized in Martin-L\"of'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.