2
$\begingroup$

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?

$\endgroup$
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy