3.8.3 of the HoTT book gives the following as a variant of the axiom of choice:
$\Pi$ (X : U) (Y : X $\rightarrow$ U), (isSet X) $\rightarrow$ ($\Pi$ (x : X), isSet (Y x)) $\rightarrow$ ($\Pi$ (x : X), $\Vert$ Y x $\Vert$) $\rightarrow$ ($\Vert$ $\Pi$ (x : X), Y x $\Vert$)
but it also comments on some possible modifications of the axiom:
The restriction in the axiom of choice to types that are sets can be relaxed to a certain extent. For instance, we may allow A and P in (3.8.1), or Y in (3.8.3), to be arbitrary type families; this results in a seemingly stronger statement that is equally consistent.
The phrase 'seemingly stronger' is confusing. Does it mean that the resulting statement is stronger? Or does it mean that the difference is only superficial, such that we can actually show
$\Pi$ (X : U) (Y : X $\rightarrow$ U), (isSet X) $\rightarrow$ ($\Pi$ (x : X), $\Vert$ Y x $\Vert$) $\rightarrow$ ($\Vert$ $\Pi$ (x : X), Y x $\Vert$)
to be equivalent to 3.8.3? Or is the equivalence of two statements an open question?
If I recall correctly, the intent of the book's phrasing was not to imply anything about whether it is actually strictly stronger. I certainly haven't ever seen a proof that 3.8.3 implies the stronger statement where $Y$ isn't a set; but I don't think I've ever seen a proof that it doesn't either. Which means that I guess it is an open problem. I suspect that one of the models in 1508.02410 could be found that would satisfy 3.8.3 but not the stronger version, but I haven't checked.