{'fraction_non_alphanumeric': 0.032679738562091505, 'fraction_numerical': 0.009150326797385621, 'mean_word_length': 4.691449814126394, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Remarks on the relation between families of setoids and identity in type theory

can be turned into a family represented by a function. This can be contrasted to MartinLöf type theory [10], and other theories of dependent types, where a family of types is a basic mathematical object. Following the tradition in constructive mathematics (see [2]) a set is commonly understood in type theory as a setoid, that is, a type together with an equivalence relation. However the notion of a family of setoids present some choices for conceptualisation. In this note we consider two choices, so-called proofirrelevant and proof-relevant families (see [3]), and their relation to the identity types of Martin-Löf. As shown by Streicher [12] and Hofmann and Streicher [6] an important distinction regarding identity types is whether their proof-objects are unique or not. In the former case a proof-irrelevant family of setoids can always be associated to each family of types. In the latter case a more involved proof-relevant notion of family of setoids seems be necessary to use; see Theorems 4.1 and 4.3. The distinction between proof-relevant and proof-irrelevant does not appear in classical set-theoretic models of Martin-Löf type theory, in view of a result by Hedberg [5] on uniqueness of identity proof-objects (UIP). We present a slight strengthening of this result in Section 6. In Section 7 we address the question whether there is a natural axiomatisation of general UIP by presenting a new elimination rule for identity types.