Krzysztof Kapulkin & Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky). Journal of the European Mathematical Society (JEMS), 23(6):2071--2126, 2021. https://doi.org/10.4171/JEMS/1050 https://arxiv.org/abs/1211.2851v5