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.
2018 (English)In: 23rd International Conference on Types for Proofs and Programs (TYPES 2017) / [ed] Andreas Abel, Fredrik Nordvall Forsberg, Ambrus Kaposi, Dagstuhl: Schloss Dagstuhl, Leibniz-Zentrum für Informatik , 2018, p. 1-7Conference paper, Published paper (Refereed)
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 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.

Place, publisher, year, edition, pages
Dagstuhl: Schloss Dagstuhl, Leibniz-Zentrum für Informatik , 2018. p. 1-7
Series
Leibniz International Proceedings in Informatics (LIPIcs), ISSN 1868-8969 ; 104
Keywords [en]
type theory, formalization, category theory, setoids
National Category
Mathematics
Research subject
Mathematical Logic
Identifiers
URN: urn:nbn:se:su:diva-164919DOI: 10.4230/LIPIcs.TYPES.2017.7ISBN: 978-3-95977-071-2 (print)OAI: oai:DiVA.org:su-164919DiVA, id: diva2:1280726
Conference
23rd International Conference on Types for Proofs and Programs (TYPES 2017), Budapest, Hungary, 29 May-1 June, 2017
Funder
Swedish Research CouncilAvailable from: 2019-01-20 Created: 2019-01-20 Last updated: 2019-02-04Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Search in DiVA

By author/editor
Palmgren, Erik
By organisation
Department of Mathematics
Mathematics

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 4 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