Re: [HoTT] What is knot in HOTT?

[Ali Caglayan <alizter@gmail.com>]

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

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.

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