Agda-2.3.2.2: test/fail/Issue464.err
Issue464.agda:23,6-7 U is not strictly positive, because it occurs in the second argument to ⟦_⟧ in the type of the constructor intro in the definition of U.
Issue464.agda:23,6-7 U is not strictly positive, because it occurs in the second argument to ⟦_⟧ in the type of the constructor intro in the definition of U.