11
$\begingroup$

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

$\endgroup$
8
$\begingroup$

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

$\endgroup$
8
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.