Is it known if "Homotopy type theory" (HTT) can consistently model objects beyond V?

373 Views Asked by At

I read the free book on HTT but could not find an answer to this question. If that were the case HTT would be stronger than ZFC+LC (for any choice of the Large Cardinal axiom). That would be because, ZFC+LC can only reach cardinals below V, and HTT would allow to an infinity taller (larger?) than ZFC+LC because it can in principle put proper classes next to another and mimic the cantor method of using ordinals after $\omega$) to define larger and larger ordinals and cardinals, which, with a simple generalization can be used to measure the sizes of collections of proper classes. Is this correct?