Why did Agda give up cumulative universes?

Question

In Ulf Norell's PhD thesis, which is considered the standard reference of the Agda 2 language, the universes are cumulative, say, Set i is not just an instance of Set (suc i), but also a subtype of it.

However, in the implementation of Agda, this is not true. We only have the "instance of" relation, not the subtype relation, until recently (--cumulativity).

IMO, it is good to have more flexibility, but why would Agda developers delete this in the beginning? What inconveniences or problems did cumulative universes bring to us?

Answer 1

One reason (not particularly specific to Agda) might be that eta reduction is not compatible with cumulativity.

With cumulativity (that is $Set_0 \leq Set_1$), and given \begin{align*} f &:= \lambda X.(\lambda Y.Y)X &: Set_0\to Set_1\\ f_\eta &:= \lambda Y.Y &: Set_1\to Set_1\\ f_\beta &:= \lambda X.X &: Set_0\to Set_0 \end{align*} we would have (and we can prove, say, in Coq) $$ f \equiv_\eta f_\eta\qquad\text{ and }\qquad f\equiv_\beta f_\beta$$ which are well-typed because $$(Set_1\to Set_1) \leq (Set_0\to Set_1)\quad\text{ and }\quad(Set_0 \to Set_0) \leq (Set_0\to Set_1) ,$$ but we have the awkward situation that $f_\eta$ is not comparable to $f_\beta$.

---

So while Coq has cumulativity but does not eta-reduce (it does eta-convert however), Agda supports eta-reduction (please correct me if this is wrong) but does not support cumulativity.