Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
Constructions of categories of setoids from proof-irrelevant families
Stockholm University, Faculty of Science, Department of Mathematics.
Number of Authors: 1
2017 (English)In: Archive for mathematical logic, ISSN 0933-5846, E-ISSN 1432-0665, Vol. 56, no 1-2, 51-66 p.Article in journal (Refereed) 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.

Place, publisher, year, edition, pages
2017. Vol. 56, no 1-2, 51-66 p.
Keyword [en]
Martin-Lof type theory, Proof-irrelevance, Category
National Category
Mathematics Computer and Information Science
Identifiers
URN: urn:nbn:se:su:diva-140300DOI: 10.1007/s00153-016-0514-7ISI: 000392295400004OAI: oai:DiVA.org:su-140300DiVA: diva2:1080972
Available from: 2017-03-13 Created: 2017-03-13 Last updated: 2017-03-13Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Palmgren, Erik
By organisation
Department of Mathematics
In the same journal
Archive for mathematical logic
MathematicsComputer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 3 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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