Dependent products preserve univalent families

Let \(\phi_{\sharp}\) be the \(T\)-indexed left adjoint of \(\phi^*\) from Lemma 4.52. The adjunction gives a natural isomorphism on arrow categories Under this isomorphism, the \(T\)-indexed condition says that any morphism \(v\to \phi^*(u)\) whose square in \(S\) is a pullback is sent to a morphism \(\phi_{\sharp}(v)\to u\) whose square in \(T\) is a pullback. Thus we get a map This map is a monomorphism of animae: both sides are subanimae of the corresponding arrow-category mapping animae, and the ambient map is an isomorphism. If \(u\) is univalent, then \(\Hom_{\Fam(T)}(\phi_{\sharp}(v),u)\) is \((-1)\)-truncated; hence its subanima \(\Hom_{\Fam(S)}(v,\phi^*(u))\) is also \((-1)\)-truncated. Thus \(\phi^*(u)\) is univalent.