Ä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
Constructions of categories of setoids from proof-irrelevant families
Stockholms universitet, Naturvetenskapliga fakulteten, Matematiska institutionen.
Antal upphovsmän: 12017 (Engelska)Ingår i: Archive for mathematical logic, ISSN 0933-5846, E-ISSN 1432-0665, Vol. 56, nr 1-2, s. 51-66Artikel i tidskrift (Refereegranskat) Published
Abstract [en]

When formalizing mathematics in constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids (types with explicit equivalence relations). In this note we consider two categories of setoids with equality on objects and show, within intensional Martin-Lof type theory, that they are isomorphic. Both categories are constructed from a fixed proof-irrelevant family F of setoids. The objects of the categories form the index setoid I of the family, whereas the definition of arrows differs. The first category has for arrows triples where f is an extensional function. Two such arrows are identified if appropriate composition with transportation maps (given by F) makes them equal. In the second category the arrows are triples where R is a total functional relation between the subobjects of the setoid sum of the family. This category is simpler to use as the transportation maps disappear. Moreover we also show that the full image of a category along an E-functor into an E-category is a category.

Ort, förlag, år, upplaga, sidor
2017. Vol. 56, nr 1-2, s. 51-66
Nyckelord [en]
Martin-Lof type theory, Proof-irrelevance, Category
Nationell ämneskategori
Matematik
Identifikatorer
URN: urn:nbn:se:su:diva-140300DOI: 10.1007/s00153-016-0514-7ISI: 000392295400004OAI: oai:DiVA.org:su-140300DiVA, id: diva2:1080972
Tillgänglig från: 2017-03-13 Skapad: 2017-03-13 Senast uppdaterad: 2018-06-19Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltext

Sök vidare i DiVA

Av författaren/redaktören
Palmgren, Erik
Av organisationen
Matematiska institutionen
I samma tidskrift
Archive for mathematical logic
Matematik

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 10 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