3 ms·

Is there anyone approaching the issue from the other side? Meaning, if I have a good understanding of programming and type theory, using that to explain homoto

• tel 12y ago
  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.