Re: [HoTT] What is knot in HOTT?

[Ali Caglayan <alizter@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2312 bytes --]

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.

[-- Attachment #1.2: Type: text/html, Size: 2986 bytes --]