# Model of homotopy type theory in ZFC

There is a model of ZFC in homotopy type theory

Does exist a model of homotopy type theory in ZFC?

Is there a proof of "equal logical expressivity" of these theories?

p.s. I use word "model" in common sense, because I don't know model theory

• The correct answer is "No", Mike, and your link indicates that. You may want to clarify what you mean. (Of course, the answer is "yes" if $\mathsf{ZFC}$ is replaced with one of its standard extensions via large cardinals, but that seems to be precisely the point of the question.) – Andrés E. Caicedo Dec 25 '15 at 22:37
• @AsafKaragila The universes here are not Grothendieck universes. The model is built starting from two Grothendieck universes. It has strength beyond $\mathsf{ZFC}$ because you can interpret set theory inside. – Andrés E. Caicedo Dec 27 '15 at 14:58