Formalization of the cumulative hierarchy V of the HoTT book (§10.5), using the Coq HoTT library ( available here: https://github.com/HoTT/HoTT )