Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
On equality of objects in categories in constructive type theory
Stockholm University, Faculty of Science, Department of Mathematics.
(English)Manuscript (preprint) (Other academic)
Abstract [en]

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.

National Category
Natural Sciences
Research subject
Mathematical Logic
Identifiers
URN: urn:nbn:se:su:diva-151874OAI: oai:DiVA.org:su-151874DiVA, id: diva2:1176015
Funder
Swedish Research Council
Available from: 2018-01-19 Created: 2018-01-19 Last updated: 2018-01-19Bibliographically approved

Open Access in DiVA

fulltext(140 kB)5 downloads
File information
File name FULLTEXT01.pdfFile size 140 kBChecksum SHA-512
185dd26c386de7e1c74a6b6a29826386c29da82424b129beebaf1a4fe4313108482b2341f460b776eab66766ef3f73c7444f676a8eebfe71d5160ac897abb3ef
Type fulltextMimetype application/pdf

By organisation
Department of Mathematics
Natural Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 5 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 6 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf