We extend Martin-Löf’s constructive set theory with effective quotient sets and the rule of uniqueness of propositional equality proofs. We prove that in the presence of at least two universes U_0 and U_1 the principle of excluded middle holds for small sets. The key point is the combination of uniqueness of propositional equality proofs with the effectiveness condition that allows us to recover information on the equivalence relation from the equality on the quotient set.
About effective quotients in constructive type theory
MAIETTI, MARIA EMILIA
1999
Abstract
We extend Martin-Löf’s constructive set theory with effective quotient sets and the rule of uniqueness of propositional equality proofs. We prove that in the presence of at least two universes U_0 and U_1 the principle of excluded middle holds for small sets. The key point is the combination of uniqueness of propositional equality proofs with the effectiveness condition that allows us to recover information on the equivalence relation from the equality on the quotient set.File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
