I think many people are approaching it that way. Ultimately you can end up using higher inductive types as "synthetic homotopy", i.e. homotopy theory which is b

I think many people are approaching it that way. Ultimately you can end up using higher inductive types as "synthetic homotopy", i.e. homotopy theory which is by construction valid to the definition instead of carefully isolated from other constructions. So you can certainly just take the type theory and start to get at pretty large stuff in actual homotopy theory.