Change search
ReferencesLink to record
Permanent link

Direct link
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
URN: urn:nbn:se:su:diva-80137DOI: 10.1007/s00153-011-0252-9ISI: 000306331000003OAI: diva2:553010


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

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 64 hits
ReferencesLink to record
Permanent link

Direct link