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