Hi! My guess would be that differentiability is irrelevant for knot theory. You could rather consider closed subsets homeomorphic to S^1. For instance you could restrict your attention to "paths" consisting of injective sequences of integral points P1, ... , Pi, ..., Pn=P0, where PiPi+1 is parallel to an axis and of length 1. There is probably a corresponding notion of "discrete" isotopy among such paths, so that if two such paths are continuously isotopic, they are also discretely isotopic . As a consequence knots now live in Z^3. So you can take the higher inductive type H with Z^3 as set of points, and the above (length one) intervals as generating equalities, and study "synthetic knots" in there. The first thing to check is probably that any path in H is homotopic to a path obtained from a sequence of generators. I am not sure at all that such a synthetic knot theory could be fruitful May-be more interesting is to fill the holes in the H above by adding generating 2-cells one for each elementary square and 3-cells one for each elementary cube. It is not so clear how to do it if you want these cells to be "invertible" More generally given a triangulated variety of dimension 3, you may try to specify as above a higher-inductive type, so that you could try to formulate (and prove...) a synthetic Poincaré conjecture. Sorry for divagating slightly too much! ah Le mer. 20 nov. 2019 à 20:13, Ali Caglayan a écrit : > It seems to me that "differentially cohesive HoTT", whatever it ends up > being, is exactly the kind of viewpoint needed to study knot theory. The > following characterisation of knot theory (I think?) due to Allen Hatcher > might make this more apparent: > > Knot theory is the study of path-components of the space of smooth > submanifolds of S^3 diffeomorphic to S^1. > > So you need to be able to talk about a space being smooth, pick a smooth > structure for S^3 and S^1, what it means to be an immersion into a manifold > (submanifold) and diffeomorphisms. This is just stating what knot theory > ought to be, I have no idea if this viewpoint can actually tell you > anything until we have some workable theory of differential cohesion. > Currently we only have real-cohesive versions of HoTT. > > Some starter questions would be: > - Can you characterize the trivial knot. > - How do you define the "connected sum" of knots. > - How do you show every knot has an "inverse" with respect to the sum. > > > On Thursday, 19 July 2018 09:55:55 UTC+1, Ali Caglayan wrote: >> >> 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. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/b886590f-c92b-493b-8751-9b0a342e9bdf%40googlegroups.com > > . > -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAHPPr6zWU1VN7J_NXTJQ6ZuLc3TjrJ7yfJwMDqPuVu005%2BJqzA%40mail.gmail.com.