# 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.