Why are quotients so much trickier in constructive type theory than in constructive set theory?

Allow me to restate part of Peter LeFanu Lumsdaine's great answer in more concrete terms. I should stress that I am not an expert at all, so I hope the actual experts will correct me if needed.

On the one hand, CZF and IZF-with-replacement have the disjunction and numerical existence properties, making them seem constructively acceptable. On the other hand, the problems we have with quotients in type theory are strongly related to how we compute with them. So where's the disconnect? In a word: canonicity.

Recall or learn that for a type theory to have the canonicity property means by definition that any closed normal term of an inductive type is headed by a constructor.

In particular, if canonicity is satisfied, by normalizing a proof of a closed proposition $∃ n ∈ ℕ. P(n)$, we get a term of the form $(n, x)$ (headed by the dependent pair constructor), and $n$ is in turn a normal term of type $ℕ$, hence a numeral, and $x$ is a proof of $P(n)$: we have the numerical existence property. Likewise we get the disjunction property. (Here I assume that $∨$ and $∃$ are inductive types as e.g. in the calculus of inductive constructions; the same applies mutatis mutandis with other variants.) But canonicity is a stronger property.

Stated very informally, type theory follows the Curry-Howard correspondence, which is an instance of the Brouwer-Heyting-Kolmogorov interpretation of proofs, and the canonicity property is a check that CH actually follows BHK. In set theory, there is no native notion of computation with proofs, so the best we can expect is simply an extraction of proofs to programs. But in type theory, we do have native computation — namely, proofs are terms, and there is a reduction relation on terms, which is a core part of the type theory because it is used to define when terms are convertible (definitional a.k.a. judgmental equality). In such a setting, we can hope that the reduction relation actually corresponds to the notion of executing the proof as a program that BHK tells us should exist. Even more informally, canonicity says that the type theory not only has a realizability model, but is its own realizability model.

Now, if we simply go through the construction of quotients we have in CZF to redo it in type theory, we have $S : \mathsf{Type}$, $E : S → S → \mathsf{Prop}$, and for $a : S$ we start by constructing the equivalence class $[a] :≡ λ x . E(a, x) : S → \mathsf{Prop}$. Next, we want to prove $E(a, b) ⇒ [a] = [b]$, so assume $E(a, b)$. In order to equate the equivalent propositions $E(a, x)$ and $E(b, x)$ for $x : A$, we need propositional extensionality. After that, in order to equate the pointwise equal functions $λ x . E(a, x)$ and $λ x . E(b, x)$, we need functional extensionality. In CZF, this is all taken care of by the set extensionality axiom $(∀ x, x ∈ a ⇔ x ∈ b) ⇒ a = b$. But type theorists don't much like simply bolting functional and propositional extensionality onto, say, the calculus of inductive constructions, because they break canonicity. (They do not break disjunction or numerical existence: basically, you can still convert terms with these axioms to executable programs, which theoreticians call interpreting in a realizability model and practitioners call code extraction. That is, for example, Rocq's extraction to OCaml, or Lean's bytecode interpreter. The point is that just reducing the terms blocks on unreducible applications of the axioms, but the extraction performs an amount of type erasure which dissolves the problem.)

Conversely, let's see why at least some amount of extensionality is necessary to have well-behaved quotients. This page of the Lean documentation shows that they entail functional extensionality. Given a type $A$ and an equivalence relation $R : A → A → \mathsf{Prop}$ on it, you certainly want that every function $f : A → B$ which respects $R$ factors through $\tilde{f} : A/R → B$, so that $\tilde{f}([x]) = f(x)$; but arguably, this should really be a definitional equality, because it is practically really annoying if it is not, and this is very similar to inductive types, for which the computation rules are always definitional. But then, consider the function space $A → B$ quotiented by $R$ the pointwise equality. For $a : A$, the function $λ (f : A → B) . f(a) : (A → B) → B$ obviously respects $R$, so it factors through a function $\mathsf{app}_a : (A → B)/R → B$ which satisfies $\mathsf{app}_a([f]) ≡ f(a)$ as a definitional equality. Then, if $f \ R \ g$, we have by η-expansion $f ≡ λ a . f(a) ≡ λ a . \mathsf{app}_a([f]) = λ a . \mathsf{app}_a([g]) ≡ λ a . g(a) ≡ g$.

This is far from the end of the story, but it does show that to get well-behaved quotients you need functional extensionality, and making that compatible with canonicity is already a major problem. To my knowledge, the only existing answer is cubical type theory, which proves univalence and in particular functional extensionality, and if I understand correctly can do quotients with higher inductive types.