Archive for Mathematical Logic 51 (1-2):35-47 (2012)

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
Keywords Martin–Löf type theory  Proof-relevance  Dependent types  Identity type
Categories (categorize this paper)
DOI 10.1007/s00153-011-0252-9
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 52,661
Through your library

References found in this work BETA

Constructive Analysis.Errett Bishop & Douglas Bridges - 1987 - Journal of Symbolic Logic 52 (4):1047-1048.

Add more references

Citations of this work BETA

Constructions of Categories of Setoids From Proof-Irrelevant Families.Erik Palmgren - 2017 - Archive for Mathematical Logic 56 (1-2):51-66.

Add more citations

Similar books and articles

Type-Identity Conditions for Phenomenal Properties.Simone Gozzano - 2012 - In Simone Gozzano & Christopher S. Hill (eds.), New Perspective on Type Identity. The Mental and the Physical. Cambridge University Press. pp. 111-126.
Cut-Elimination for Simple Type Theory with an Axiom of Choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
Implicational F-Structures and Implicational Relevance Logics.A. Avron - 2000 - Journal of Symbolic Logic 65 (2):788-802.
Is Type Identity Incompatible with Multiple Realization?Michael Pauen - 2002 - Grazer Philosophische Studien 65 (1):37-49.
Mind-Brain Correlations, Identity, and Neuroscience.Brandon N. Towl - 2012 - Philosophical Psychology 25 (2):187 - 202.
A Type Reduction From Proof-Conditional to Dynamic Semantics.Tim Fernando - 2001 - Journal of Philosophical Logic 30 (2):121-153.
Story Identity and Story Type.Aaron Smuts - 2009 - Journal of Aesthetics and Art Criticism 67 (1):5-14.


Added to PP index

Total views
71 ( #132,314 of 2,339,983 )

Recent downloads (6 months)
1 ( #516,585 of 2,339,983 )

How can I increase my downloads?


My notes