Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat 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 (Engelska)Ingå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-7Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
Dagstuhl: Schloss Dagstuhl, Leibniz-Zentrum für Informatik , 2018. s. 1-7
Serie
Leibniz International Proceedings in Informatics (LIPIcs), ISSN 1868-8969 ; 104
Nyckelord [en]
type theory, formalization, category theory, setoids
Nationell ämneskategori
Matematik
Forskningsämne
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
Konferens
23rd International Conference on Types for Proofs and Programs (TYPES 2017), Budapest, Hungary, 29 May-1 June, 2017
Forskningsfinansiär
VetenskapsrådetTillgänglig från: 2019-01-20 Skapad: 2019-01-20 Senast uppdaterad: 2022-02-26Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltext

Person

Palmgren, Erik

Sök vidare i DiVA

Av författaren/redaktören
Palmgren, Erik
Av organisationen
Matematiska institutionen
Matematik

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 74 träffar
RefereraExporteraLänk till posten
Permanent länk

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