13
$\begingroup$

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?

$\endgroup$

1 Answer 1

14
$\begingroup$

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.

$\endgroup$
9
  • 2
    $\begingroup$ 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. $\endgroup$ Feb 10, 2022 at 5:18
  • 2
    $\begingroup$ You example relies on having annotated abstractions, and indeed it is part of the reasons why having η in the reduction is problematic in Coq. But Agda’s abstractions are unannotated, so the issue should disappear… $\endgroup$ Feb 10, 2022 at 11:53
  • 2
    $\begingroup$ Doesn't this argument apply to subtyping in general? Current Agda has a limited amount of subtyping, so this can't be a fatal issue. $\endgroup$
    – James Wood
    Feb 10, 2022 at 13:42
  • 3
    $\begingroup$ This seems just another example of "eta-reduction is broken (even without cumulativity), use (type-directed) eta-expansion", which I think is what Agda uses. $\endgroup$ Feb 16, 2022 at 10:05
  • 2
    $\begingroup$ In fact, Agda does have eta-reduction (at least for records!), but it's still unsound: github.com/agda/agda/issues/2732. $\endgroup$ Feb 20, 2022 at 13:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.