Remark 4.48.
This construction is the join construction for propositional truncation, transplanted from homotopy type theory to the category \(\Fam(T)\); compare [Uemura 2025, Proposition 4.7].
References
- Taichi Uemura. Colimits in the ∞-category of ∞-topoi and étale morphisms. 2025.