There is a correspondence between univalence in Type Theory and object classifiers in $\infty$-toposes. This, for example, is suggested in the article Univalent Foundations for Mathematics on nlab.
Section 4.8 of the HoTT book describes how univalent universes $\mathcal U$ give rise to object classifiers in Type Theory
$$\require{AMScd}
\begin{CD}
A @>{\theta_f}>> \mathcal U_\bullet\\
@V{f}VV @VV{\texttt{pr}}V \\
B @>>{\chi_f}> \mathcal U
\end{CD}$$
where $ \mathcal U_\bullet :\equiv \sum_{A \, : \, \mathcal U} A $ is the type of pointed types and $ \texttt{pr} $ the corresponding projection, $ A : \mathcal U $ and
\begin{equation}
\chi_f(b) \equiv \texttt{fib}_f(b), \qquad \theta_f(a) \equiv \big( \texttt{fib}_f(f \, a), (a,\texttt{refl}_{f \,a}) \big).
\end{equation}
Does the other direction also hold? Is it possible to show that a universe $ \mathcal U$ in Martin-Löf Type Theory is univalent, assuming that the canonical projection $ \texttt{pr} : \sum_{A\, : \, \mathcal U} A \to \mathcal U $ is an object classifier in the sense of section 4.8 of the HoTT book?
A naive idea I have considered is to put the function $ \texttt{idtoeqv} : (A=_{\mathcal U} B) \to (A \simeq B) $, or $ \texttt{i} $ for short, on the left of the pullback,* as in the following diagram
$$\require{AMScd}
\begin{CD}
A=_{\mathcal U} B @>>> \mathcal U_\bullet\\
@V{\texttt{i}}VV @VV{\texttt{pr}}V \\
A \simeq B @>>{\chi_\texttt{i}}> \mathcal U
\end{CD}$$
hoping that $ \chi_{\texttt{i}} $ factors through $ \texttt{pr}$, so that the universal property of the pullback will produce a candidate for the quasi-inverse. This approach failed however, since given an $ f : A \simeq B$, I must already have a path $ p : A =_{\mathcal U} B $ in the fiber $\texttt{fib}_{\texttt{i}}(f)$ at hand, in order to define the factorization $ (A \simeq B) \to \mathcal U_\bullet$ in the first place.
*Here I'm assuming that the universe is closed under identity types, i.e. $ A =_{\mathcal U} B : \mathcal U $. It sounds like a desirable property for a universe to have, but I don't know if this is included in Homotopy Type Theory or if this leads to any problems.
Best Answer
Since you said "object classifier in the sense of section 4.8", I'm going to assume that the other lemmas in that section - in particular, lemma 4.8.3, are fair game. It should be possible to recover it from 4.8.4, but I haven't formalised that.
As far as I can tell, it's not possible to prove univalence from just the lemmas in this section; You also appear need propositional extensionality and function extensionality. Using these three assumptions, we can establish univalence as follows:
We have a function $\chi : (\sum_{(A : \mathcal{U})} (A \to B)) \to B \to \mathcal{U}$, which by lemma 4.8.3 is an equivalence. Recall that this function is $\lambda\ (E , f)\ x. \mathrm{fibre}_f(x)$. We can use this result to conclude that "maps with $P$-fibres", for our choice of $P$, are classified by the object $\sum_{(A : \mathcal U)}P(A)$. For this, let $P : \mathcal{U} \to \mathcal{U}$ be a predicate on types, and observe that lemma 4.8.3 + some pair munging gives us the following chain of equivalences
Where we go from the first line to the second by rearranging pairs (associativity of $\sum$; exercise 2.10), from the second to the third using our equivalence $\chi$ on the index type (exercise 2.17), and the last uses the "type-theoretic axiom of choice", theorem 2.15.7, applied backwards.
We know that the equivalences are precisely the maps with contractible fibres (theorem 4.4.5); We will show that the type $\sum_{(A : \mathcal{U})} A \simeq B$ is contractible. Using the equivalence above, and the closure of h-levels under retracts, we can reduce this to showing
$$ \mathrm{isContr}\ (B \to \sum_{(A : \mathcal{U})} \mathrm{isContr}(A)) $$
By our assumption of function extensionality, it suffices to show that the codomain type is contractible; Since a contractible type is an inhabited proposition, it suffices to show that it is a proposition (it is inhabited by the unit type). For this, let $(A, c)$ and $(B, c')$ be two contractible types (and the witnesses that they are contractible): we have maps $A \to B$ (resp $B \to A$) sending everything to the centre of contraction of $B$ (resp $A$), so by propositional extensionality, $A = B$; Since $\mathrm{isContr}$ is a family of propositions, the claimed result follows.
We now know that $\sum_{(A : \mathcal{U})} A \simeq B$ is contractible, and since the map $(-)^{-1} : (A \simeq B) \to (B \simeq A)$ is an equivalence, so is $\sum_{(A : \mathcal{U})} B \simeq A$; To show that $\mathrm{pathToEquiv}$ is an equivalence, it suffices to show it induces an equivalence of total spaces (theorem 4.7.6), i.e. we need
$$ \left(\sum_{(A : \mathcal{U})} (B \simeq A)\right)\simeq \left(\sum_{(A : \mathcal{U})} (B = A)\right) $$
But we've just established that the left-hand-side type is contractible, and the right-hand type is contractible by path induction, so we are done. I do not know if it's possible to show univalence from the existence of an object classifier without the use of function and propositional extensionality, but I suspect that it isn't. As for the adequacy of this proof, funext and propext hold in any $(\infty,1)$-topos.
Apologies for the use of monospaced text, I couldn't get
arrayto render properly. I've also formalised this argument in Cubical Agda, avoiding the fact that univalence is a theorem. In particular, the file begins with a postulate for lemma 4.8.3, and a postulate of propositional extensionality: You can check it out here.Quick edit: While universe types aren't directly closed under paths, they are essentially closed under paths, in that while $A =_\mathcal{U} B$ is a large type, it is equivalent to the small $A \simeq B$. (I can't comment, my account is new)