Corollary 4.46. ([Uemura 2025, Corollary 4.6])
Let \(u_{\bullet}\colon [\omega] \to \Fam(T)\) be a sequence of univalent families. Then \(\colim_n u_n\) is univalent.
Proof
By Proposition 4.45, we have The diagonal functor \([\omega] \to [\omega]\times[\omega]\) is final, so this is further equivalent to \(\colim_n (u_n\times u_n)\). The diagonal of \(\colim_n u_n\) is therefore the colimit of the diagonals \(u_n \to u_n\times u_n\), which are isomorphisms by univalence.
\[\left(\colim_n u_n\right)\times\left(\colim_m u_m\right)
\simeq
\colim_{(n,m)\in [\omega]\times[\omega]}(u_n\times u_m).\]
(1)References
- Taichi Uemura. Colimits in the ∞-category of ∞-topoi and étale morphisms. 2025.