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

Yes, as long as by "ZFC" you include its extension with some inaccessible cardinals, or (perhaps) are willing to play games with natural models. In other words, the only difference in consistency strength is that "ZFC" by default doesn't include any universes, while "HoTT" by default includes countably many.