Re: [HoTT] What is knot in HOTT?

[Egbert Rijke <e.m.rijke@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2323 bytes --]

Dear Jose,

One idea I have been playing around with is to define a knot to consist of
a map S1 -> S3 together with a type X equipped with maps S1 x S1 -> X and X
-> S3, and a homotopy witnessing that the square

S1 x S1 ----------> X
   |                |
   |                |
   V                V
  S1 -------------> S3

commutes, and is a pushout square. The idea is that a knot is a topological
embedding of S1 into S3. We can fatten its image up to an embedding from S1
x D2 -> S3, where D2 is the unit disc. Its boundary is the torus S1 x S1,
and the embedding S1 x D2 -> S3 also has a complement. Then S3 should be
the homotopy pushout of S1 and the complement of the subspace S1 x D2 in S3.

The problem is of course representing known knots in this way, which I
don't really know how to do. For example, what is the homotopy type of the
complement of the trefoil. This is probably known in the existing
literature about knots, but I must admit that I don't know it. And also,
what is the embedding S1 -> S3 for the trefoil knot? The fiber inclusion of
the Hopf fibration perhaps? That would be a guess.

I would be very interested to hear if others have ideas on this topic. And
just to repeat myself, I also don't know for sure if the above is a correct
representation of a knot in HoTT.

With kind regards,
Egbert

On Thu, Jul 19, 2018, 1:18 AM José Manuel Rodriguez Caballero <
josephcmac@gmail.com> wrote:

> Dear HoTT group,
>   I'm thinking in the following question: What is the type-theoretic
> definition of a knot in HoTT?
>
> Thank you in advance if you have some answers.
>
> Sincerely yours,
> Jose Manuel Rodriguez Caballero
>
> --
> 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.
>

-- 
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 #2: Type: text/html, Size: 3732 bytes --]