From what I have seen knot-theory has been very resistant to homotopy theoretic ideas (not classical ones). One 'clean' way of working with knot theory is to do so in the context of differential geometry. Cohesive HoTT supposedly can develop adequate differential geometry but at the moment it is very undeveloped. One of the difficulties with knot theory is that (classical) homotopy theory in HoTT isn't really done with real numbers and interval objects, which is needed if you want to define notions of ambient isotopy and such. I think the main difficulty here might be that HoTT is great at doing (synthetic) homotopy but not topology. The two can be easily confused. How do you take the complement of a space for example? I could be wrong however but this is the conclusion I got when I tried thinking about HoTT knots. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.