How to construct complement of NFA universality?

Consider the language $ALL_{NFA} = \{\langle A\rangle: \text{$A$ is an NFA with $L(A) = \Sigma^*$}\}$.

If you want a non-PTIME reduction from $\overline{ALL_{NFA}}$ to $ALL_{NFA}$, then you can simply do the following naive approach. On input $\langle A\rangle$ for the reduction, the reduction checks whether $L(A) \neq \Sigma^*$, and outputs an NFA $B$ that accepts all its inputs only when $L(A)\neq \Sigma^*$. Clearly, this works but comes at a high cost: we are deciding $\overline{ALL_{NFA}}$ to output the NFA $B$ accordingly. As the non-universality check can be performed in PSPACE, the latter reduction is a PSPACE reduction. More abstractly, if you don't care about the complexity of the reduction, you can use the fact that every non-trivial language is $R$-hard (see my answer here).

I am not aware of a simple PTIME reduction from $\overline{ALL_{NFA}}$ to $ALL_{NFA}$. There is ofcourse a PTIME reduction that goes through Savitch's theorem which states that for any function $f\in \Omega(log n)$, it holds that $NPSPACE[f(n)]\subseteq SPACE[f^2(n)]$. Indeed, it is well-known that the latter theorem implies that PSPACE = NPSPACE, and since PSAPCE = coPSPACE, we get in total that NPSPACE = coNPSPACE. The latter allows us to show that $ALL_{NFA}$ is PSPACE-complete -- membership in PSPACE follows from Savitch's theorem and the fact that $\overline{ALL_{NFA}}\in \text{PSPACE}$, see for example here. Then, PSPACE-hardness is well-known and can be shown directly, see for example here. Putting everything together, we get the exsitence of a PTIME reduction from $\overline{ALL_{NFA}}$ to $ALL_{NFA}$. Is there a simpler direct redcution? Who knows, maybe (and I would like to see one), but I suspect that the output NFA of that reduction needs to be at least of quadratic size, but I am not sure. I tried to use Savitch's theorem to show the latter, but then noted that Savitch's theorem has no known tight lower bound -- see here.