About effective quotients in constructive type theory

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.