* Preprint available: On equality of objects in categories in constructive type theory
@ 2017-08-05 20:26 Erik Palmgren
0 siblings, 0 replies; only message in thread
From: Erik Palmgren @ 2017-08-05 20:26 UTC (permalink / raw)
To: homotopytypetheory
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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2017-08-05 20:27 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-08-05 20:26 Preprint available: On equality of objects in categories in constructive type theory Erik Palmgren
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).