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
Proof relevance of families of setoids and identity in type theory
Stockholm University, Faculty of Science, Department of Mathematics.
2012 (English)In: Archive for mathematical logic, ISSN 0933-5846, E-ISSN 1432-0665, Vol. 51, no 1-2, 35-47 p.Article in journal (Refereed) Published
Abstract [en]

Families of types are fundamental objects in Martin-Lof type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. A similar result is shown for fibre representations of families. The ubiquitous role of proof-irrelevant families is discussed.

Place, publisher, year, edition, pages
2012. Vol. 51, no 1-2, 35-47 p.
Keyword [en]
Martin-Lof type theory, Proof-relevance, Dependent types, Identity type
National Category
Mathematics
Identifiers
URN: urn:nbn:se:su:diva-80137DOI: 10.1007/s00153-011-0252-9ISI: 000306331000003OAI: oai:DiVA.org:su-80137DiVA: diva2:553010
Note

AuthorCount:1;

Available from: 2012-09-17 Created: 2012-09-12 Last updated: 2017-12-07Bibliographically 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
Mathematics

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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