@mildsunrise @joshchen They assume the existence of a model of ZF + ω inaccessibles:
https://github.com/leanprover/con-leche/blob/master/OVERVIEW.md#7-the-set-theory-assumption
This is similar to MetaRocq assuming that PCUIC is strongly normalizing.