Surjection from a type to a universe We work in homotopy type theory. Can there be a type $A:U_m$ and a map $f:A\to U_n$ for some $n\geq m$ such that the type $\prod_{T:U_n} \|\mathrm{fib}_f(T)\|$ is inhabited?
No, there can't be such a surjection. Here's how to derive a contradiction, if there is a surjective map $f : A \to U_n$, where $A:U_m$.
Since $m\leq n$, we can pull $f$ back along the embedding $U_m \to U_n$. This gives a surjective map $f' : A' \to U_m$, and it is not hard to see that the type $A'$ is equivalent to a type in $U_m$. Thus we have a surjective map from a type (equivalent to a type) in $U_m$ into $U_m$, and the join construction can be applied with these hypotheses to conclude that the type $U_m$ itself is equivalent to a type in $U_m$. This is well-known to lead to a contradiction.