Elementary \(\infty\)-toposes from type theory Daniël Apol, Maximilian Petrowitsch arXiv preprint, 2025