Extending Kan fibrations, without using minimal fibrations

Question

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

Answer 1

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).

Answer 2

Yes, see Corollary 7.7 in Sattler's The Equivalence Extension Property and Model Structures.

Answer 3

Despite having left academia, I still work on this problem from time to time, and I (hope I) recently worked out a combinatorial proof for the base case of extension along a horn inclusion:

https://github.com/woupiestek/really-hot/blob/master/fibrant-universes.tex

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.

The category of assemblies has a full internal subcategory--the modest sets--and I believe that the bundle of 'modest Kan complexes' is an interesting model for homotopy type theory--one that could serve as a counterexample to many Grothendieck-topos based intuitions. Four years ago, there was too little work in constructive simplicial homotopy for me to build on. It is good to see that much progress has been made in this area.