2026-07-20T11:15:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10055 2024-03-06T10:42:59Z ddc:004 open_access

On Equality of Objects in Categories in Constructive Type Theory Palmgren, Erik type theory formalization category theory setoids 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Erik Palmgren 2019 Is Part Of LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2017.7 urn:nbn:de:0030-drops-100553 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.7 eng https://creativecommons.org/licenses/by/3.0/legalcode