Name
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/s00153-011-0252-9 | Arch. Math. Log. |
Keywords | Field | DocType |
fundamental object,proof-relevant family,similar result,proof-irrelevant indexing,fibre representation,equivalence relation,type theory,proof-irrelevant family,general proof-irrelevant,identity type,mathematics | Setoid,Discrete mathematics,Equivalence relation,Intuitionistic type theory,Type theory,Pure mathematics,If and only if,Mathematics | Journal |
Volume | Issue | ISSN |
51 | 1-2 | 1432-0665 |
Citations | PageRank | References |
2 | 0.52 | 4 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Erik Palmgren | 1 | 233 | 43.17 |