$\require{AMScd}$One thing that needs to be checked to give an interpretation of type theory in simplicial sets (as in Kapulkin-Lumsdaine) is that "the base of the universal fibration is fibrant". Expanding the definitions reduces this to the following statement.

$(*)$ Given a Kan fibration $p : X \to A$ and an acyclic cofibration $i : A \to B$, there exists a square $$ \begin{CD} X @>j>> Y \\ @V p VV @VV q V \\ A @>>i> B \end{CD} $$ in which $q$ is a Kan fibration and the square is a pullback square.

It suffices to handle the case when $i : A \to B$ is one of the generating acyclic cofibrations $\Lambda^n_k \to \Delta^n$.

I have seen only one proof of $(*)$, which relies on the theory of minimal fibrations. I'm wondering about alternative approaches, so my main question is

Are there proofs of $(*)$ which do not use minimal fibrations?

In particular, a probably related question is whether, for fixed $i : A \to B$, the construction in $(*)$ can be carried out functorially in $X$ in an appropriate sense.

Observe that in a square such as in $(*)$, the map $j$ is automatically an acyclic cofibration (it is a monomorphism, and a weak equivalence because $\mathrm{SSet}$ is right proper). So $X \xrightarrow{j} Y \xrightarrow{q} B$ is an acyclic cofibration-fibration factorization of $ip : X \to B$, but with the added constraint that $j : X \to Y$ can only attach simplices which live above $B \setminus A$. Perhaps it is possible to modify a known method for constructing factorizations so that it adheres to this additional constraint?