Univalent completion

Let \(u\) be a family. We construct a sequence \(u_0 \to u_1 \to u_2 \to \cdots\) in \(\Fam(T)\) by setting \(u_0=u\) and defining \(u_{n+1}\) by the pushout square

Let \(u_{\infty}:=\colim_n u_n\). We claim that \(u_{\infty}\) is univalent. Indeed, the pushout square gives a canonical map \(q_n\colon u_n\times u_n \to u_{n+1}\) for which both composites \(u_n\rightrightarrows u_n\times u_n \to u_{n+1}\) agree with the structure map \(u_n\to u_{n+1}\). In other words, \(q_n\) is a diagonal filler for

Moreover, the composites are the structure maps of the shifted sequence \((u_{n+1})_n\) and of the sequence \((u_n\times u_n)_n\), respectively. Since the shift \([\omega]_{\geq 1}\hookrightarrow [\omega]\) is final, and since (4.1) holds without assuming the \(u_n\) are univalent, passing to colimits identifies the resulting map with the diagonal and the maps \(q_n\) induce an inverse. Hence this diagonal is an isomorphism.Now let \(v\) be a univalent family. We show that restriction along \(u \to u_{\infty}\) induces an equivalence Given a map \(u_n \to v\), the two induced maps \(u_n\times u_n \rightrightarrows v\) agree because \(v\) is \((-1)\)-truncated in \(\Fam(T)\). Hence the map \(u_n \to v\) extends uniquely across the pushout defining \(u_{n+1}\). Iterating and passing to the limit gives the desired isomorphism. This proves the adjunction.