Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
On equality of objects in categories in constructive type theory
Stockholms universitet, Naturvetenskapliga fakulteten, Matematiska institutionen.
2018 (engelsk)Inngår i: 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, s. 1-7Konferansepaper, Publicerat paper (Fagfellevurdert)
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.

sted, utgiver, år, opplag, sider
Dagstuhl: Schloss Dagstuhl, Leibniz-Zentrum für Informatik , 2018. s. 1-7
Serie
Leibniz International Proceedings in Informatics (LIPIcs), ISSN 1868-8969 ; 104
Emneord [en]
type theory, formalization, category theory, setoids
HSV kategori
Forskningsprogram
matematisk logik
Identifikatorer
URN: urn:nbn:se:su:diva-164919DOI: 10.4230/LIPIcs.TYPES.2017.7ISBN: 978-3-95977-071-2 (tryckt)OAI: oai:DiVA.org:su-164919DiVA, id: diva2:1280726
Konferanse
23rd International Conference on Types for Proofs and Programs (TYPES 2017), Budapest, Hungary, 29 May-1 June, 2017
Forskningsfinansiär
Swedish Research CouncilTilgjengelig fra: 2019-01-20 Laget: 2019-01-20 Sist oppdatert: 2022-02-26bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekst

Person

Palmgren, Erik

Søk i DiVA

Av forfatter/redaktør
Palmgren, Erik
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 74 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf