Proof relevance of families of setoids and identity in type theory
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
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.
Martin-Lof type theory, Proof-relevance, Dependent types, Identity type
IdentifiersURN: urn:nbn:se:su:diva-80137DOI: 10.1007/s00153-011-0252-9ISI: 000306331000003OAI: oai:DiVA.org:su-80137DiVA: diva2:553010