# Why did Agda give up cumulative universes?

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?

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$$.
• I don't agree with your first displayed $\eta$-equivalence. $\eta$-conversion is fundamentally a typed notion; it can't equate your LHS of type $\rm Set_0 \to Set_0$ with your RHS of type $\rm Set_1 \to Set_1$. Also I don't know what you mean by "Coq does not eta-reduce"; since quite some time ago Coq does have definitional $\eta$-conversion. Feb 10, 2022 at 5:18