# Extending Kan fibrations, without using minimal fibrations

$$\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?

A different proof, which works in much more generality, appears as part of Theorem 5.22 in my paper All (∞,1)-toposes have strict univalent universes: factor the composite $$X\to A\to B$$ as an acyclic cofibration $$X \to Z$$ followed by a fibration $$Z\to B$$, deduce from right properness and 2-out-of-3 that $$X\to i^*Z$$ is a weak equivalence, then use the equivalence extension property to find a fibration $$Y\to B$$ that is (equivalent to $$Z$$ and satisfies) $$i^*Y \cong X$$. As far as I know this proof was only recently noticed, independently by various people (myself, Peter Lumsdaine, and Raffael Stenzel are the ones that I know about).
I want these constructions to work for realizability toposes and related categories--in particular for the category of simplicial assemblies. In that case, monics aren't necessarily cofibrations as in Karol's paper and horns aren't necessarily $$\kappa$$-representable for any classical cardinality as in Mike's paper, hence the complicated workaround.