Univalent completion (Q1659918)

A Kan fibration \(p\) of simplicial sets is called \textit{universal} if every fibration satisfying a certain set-theoretic size restriction (typically on the cardinality of the fibre) is a homotopy pullback of \(p\). The fibration \(p\) is called \textit{univalent} if, roughly speaking, the path space of the base of \(p\) is weakly equivalent to the space of (parametrised) weak equivalences between fibres of \(p\). In the paper under review, the authors prove in Theorem 2 that for any fibration \(E \rightarrow B\) there exists a univalent fibration \(E' \rightarrow B'\) (in the same set-theoretic universe) with \(B \subseteq B'\), together with a map of fibrations resulting in a homotopy pullback square (so that the map \(E \rightarrow B \times_{B'} E'\) is a weak equivalence): \[ \begin{matrix} E & \rightarrow & E' \\ \downarrow && \downarrow \\ B & \subseteq & B' \end{matrix} \] Moreover, if \(p\) is universal then \(p'\) is universal as well. The paper uses the machinery of actions of simplicial groupoids on simplicial sets, developed in \S\S2--3. Universality and univalence are discussed in \S4, and \S5 is devoted to the formulation and proof of Theorem 2. The paper requires no background in type theory. It is carefully written and self-contained, assuming only familiarity with basic homotopy theory of simplicial sets.