Я не могу решить ошибку "Вселенные не связаны"

Question

Я разрабатываю библиотеку для гугологии в Coq. Я столкнулся с проблемой.

Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.

Inductive Sum@{i j} (A : Type@{i}) (B : Type@{j}) : Type@{max(i,j)}
  := left : A -> Sum A B | right : B -> Sum A B.

Definition Foo@{i j k l} (A : Type@{i}) (B : Type@{j}) (C : Type@{k}) : Type@{l}
  := Sum@{i _} A (Sum@{j k} B C).

Я ожидал, что _ будет заполнено max(j,k). Тем не менее, я получил ошибку:

Universes {***} are unbounded.

Есть ли способ хорошо express эти ограничения?

Answer 1

Мне кажется, имеет смысл добавить ij, которое удовлетворяет i <= ij и j <= ij. Я должен был подумать больше.