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.