Unset Strict Universe Declaration.
Inductive quotient {A : Type@{i}} {B : Type@{j}} : Type@{max(i, j)} := .