We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Proof-relevance of families of setoids and identity in type theory.
- Authors
Palmgren, Erik
- Abstract
Families of types are fundamental objects in Martin-Löf 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.
- Subjects
PROOF theory; TYPE theory; MATHEMATICAL logic; SET theory; EQUIVALENCE relations (Set theory); MATHEMATICAL analysis
- Publication
Archive for Mathematical Logic, 2012, Vol 51, Issue 1/2, p35
- ISSN
0933-5846
- Publication type
Article
- DOI
10.1007/s00153-011-0252-9