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
(Σ[ A ∈ Type _ ] Σ[ f ∈ (A → B) ] ((x : B) → P (fibre f x))) ≃
(Σ[ (x , f) ∈ Σ[ A ∈ Type _ ] (A → B) ] ((x : B) → P (fibre f x))) ≃
(Σ[ A ∈ (B → Type _) ] ((x : B) → P (A x))) ≃
(B → Σ P)
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 array to 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)
Best Answer
I'm not exactly sure what you think the difficulty is. Here are some (supersets of) models that come to mind, although I admit they're not super precise:
In fact, Martin-löf has a variation of type theory, extensional type theory, that has extensional equality of functions and, necessarily, uniqueness of identity proofs (this is because the identity type gets 'reflected' back into the judgmental equality, rather than using something like the J rule, which kind of erases any structure). It's just as constructive as intensional type theory.
If you want something that looks more like intensional type theory, there was extensive work years ago on "Observational Type Theory" (OTT) by several people. The goal there was to have something that is recognizably like intensional type theory, in that it has something like the J rule for making use of identity proofs, but allow more extensional principles to be included in the identity type, like function extensionality. There was also a story for quotients and coinductive types, I believe. And it also had uniqueness of identity proofs, because that makes certain things 'easy.'
In fact, I think you can kind of see OTT as a precursor to cubical type theory (CTT). A major difference is that CTT is a lot more complicated because it doesn't have uniqueness of identity proofs, and has to have all sorts of constructions that make sure computationally relevant information is passed around and accessible in the identity types. OTT was able to get away without any of this, because any higher structure was intended to be crushed, so the main trick was to ensure that no one actually computationally depended on the value of an identity type. Instead CTT has to actually represent all this computationally relevant information.
Looping back to the models, people actually do #2 manually in e.g. Coq, using setoids to have the notion of 'equality' they actually want, when the intensional equality is not good enough. So obviously that is useful to some people.
However, if (as seems like might be implicit in your question) you think that homotopy/cubical type theory is useless to 'normal' computer scientists as long as there is an intensional type theory with function extensionality and UIP (and quotients, and ...), I think that's mistaken.