[-- Attachment #1: Type: text/plain, Size: 515 bytes --] 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. [-- Attachment #2: Type: text/html, Size: 778 bytes --]

[-- 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 --]

[-- 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 --]

This does seem like the kind of problem that Cohesive HoTT is designed to solve. You could define a knot in a purely topological way as a map from the topological circle to the topological 3-sphere, fatten it up into a tubular neighborhood to express the topological 3-sphere as a pushout of the tubular neighborhood of the topological circle and a complement, then apply the shape functor which preserves pushouts to obtain the homotopy-theoretic data described by Egbert with the homotopical 3-sphere as a pushout of the homotopical circle and some other space. On Thu, Jul 19, 2018 at 1:55 AM, Ali Caglayan <alizter@gmail.com> 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. > 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 #1.1: Type: text/plain, Size: 461 bytes --] Quillen identified the complement of the trefoil knot with SL(2,R)/SL(2,Z), and the proof is on page 84 of Milnor's book "Introduction to algebraic K-theory". -- 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: 666 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1365 bytes --] Just for the record, a trivial but nice observation: the unknot is the representation of S3 as the join of S1 with itself: p2 S1 x S1 ------> S1 | | | p1 | V V S1 ---------> S3 Unfortunately, no-one has studied SL(2,R) and SL(2,Z) in HoTT yet. Although a trival way to obtain them is through cohesive HoTT would be nice if it were possible to define these spaces directly as higher inductive types. Best, Egbert On Thu, Jul 19, 2018 at 1:56 PM, Daniel R. Grayson < danielrichardgrayson@gmail.com> wrote: > Quillen identified the complement of the trefoil knot with > SL(2,R)/SL(2,Z), and the proof is > on page 84 of Milnor's book "Introduction to algebraic K-theory". > > -- > 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. > -- egbertrijke.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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 3094 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2022 bytes --] Maybe the connection between knots and primes can be stated in terms of SL(2,R) and SL(2,Z), because these groups are essential in number theory, e.g., modular forms, quadratic forms. José M > On Jul 19, 2018, at 2:38 PM, Egbert Rijke <e.m.rijke@gmail.com> wrote: > > Just for the record, a trivial but nice observation: the unknot is the representation of S3 as the join of S1 with itself: > > p2 > S1 x S1 ------> S1 > | | > | p1 | > V V > S1 ---------> S3 > > Unfortunately, no-one has studied SL(2,R) and SL(2,Z) in HoTT yet. Although a trival way to obtain them is through cohesive HoTT would be nice if it were possible to define these spaces directly as higher inductive types. > > Best, > Egbert > >> On Thu, Jul 19, 2018 at 1:56 PM, Daniel R. Grayson <danielrichardgrayson@gmail.com> wrote: >> Quillen identified the complement of the trefoil knot with SL(2,R)/SL(2,Z), and the proof is >> on page 84 of Milnor's book "Introduction to algebraic K-theory". >> -- >> 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. > > > > -- > egbertrijke.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. > 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: 4468 bytes --]

On 7/19/18, Michael Shulman <shulman@sandiego.edu> wrote: > This does seem like the kind of problem that Cohesive HoTT is designed > to solve. Indeed, or rather that "differentially cohesive HoTT" is designed to solve: The space of equivalence classes of knots of shape Sigma(= S^1) in X(=S^3) should be the 0-truncation of the "shape" of the sub-type of the function type Sigma -> X on those that are embeddings of smooth manifolds. We may formalize "smooth manifold" types Sigma, X and "embedding of smooth manifolds" in HoTT using an "infinitesimal shape modality" "Im", as in Felix Wellen's work ncatlab.org/schreiber/show/thesis+Wellen to produce a type (Sigma -> X)_emb Then applying a shape modality to this shape (Sigma -> X)_emb yields a type whose paths should be interpreted as smooth isotopies. Hence the 0-truncation of this type Knot_Sigma(X) := | shape (Sigma -> X)_emb |_0 should be the type of equivalence classes of Sigma-shaped knots in X. This would make sense for any Sigma and X. Indeed, the main problem from this angle seems to be to axiomatize the generic manifold types Sigma and X to behave enough like S^1 and S^3 such that one can draw usual conclusions. Not sure about that. One might be tempted to use Mike's "real cohesion", but that probably does not admit a non-trivial "infinitesimal shape modality" (being based on the topological real line, instead of the smooth one). Incidentally, just yesterday I tentatively started compiling a list with "open problems and further directions in cohesive homotopy theory". Just added a brief item on knot theory there: https://ncatlab.org/schreiber/show/Some+thoughts+on+the+future+of+modal+homotopy+type+theory#KnotTheory Related discussion on the nForum https://nforum.ncatlab.org/discussion/8747/open-problems-in-axiomatic-cohesion/#Item_1 Best wishes, urs -- 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.

On Fri, Jul 20, 2018 at 3:27 AM, 'Urs Schreiber' via Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com> wrote: > Indeed, the main problem > from this angle seems to be to axiomatize the generic manifold types > Sigma and X to behave enough like S^1 and S^3 such that one can draw > usual conclusions. Once we have the "smooth real numbers", wouldn't we just define S^1 and S^3 in terms of them as usual? Or are you saying that the problem is in characterizing the smooth reals inside differential cohesion? -- 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.

> Once we have the "smooth real numbers", wouldn't we just define S^1 > and S^3 in terms of them as usual? Or are you saying that the problem > is in characterizing the smooth reals inside differential cohesion? Yes. Possibly one could make progress by declaring shape to be homotopy localization at some type A^1 of which we only demand that it be homogeneous (as in Def. 4.8 in arxiv.org/abs/1806.05966) and then focus attention on A^n-manifolds (as in Def. 7.1). One could maybe declare that a smooth n-sphere to be an A^n-manifold whose shape is equivalent to Disc(S^n). Classically, this should work away from dimensions in which there are exotic spheres, hence in particular for the case n <= 3 of relevance in knot theory. Best wishes, urs -- 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.

It seems to me that especially if we want to construct *particular* knots, we would need the smooth reals to at least be a ring and probably to support trigonometric functions. On Fri, Jul 20, 2018 at 6:45 AM, 'Urs Schreiber' via Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com> wrote: >> Once we have the "smooth real numbers", wouldn't we just define S^1 >> and S^3 in terms of them as usual? Or are you saying that the problem >> is in characterizing the smooth reals inside differential cohesion? > > Yes. > > Possibly one could make progress by declaring shape to be homotopy > localization at some type A^1 of which we only demand that it be > homogeneous (as in Def. 4.8 in arxiv.org/abs/1806.05966) and then > focus attention on A^n-manifolds (as in Def. 7.1). > > One could maybe declare that a smooth n-sphere to be an A^n-manifold > whose shape is equivalent to Disc(S^n). Classically, this should work > away from dimensions in which there are exotic spheres, hence in > particular for the case n <= 3 of relevance in knot theory. > > Best wishes, > urs > > -- > 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.

Of course, braids, knots and tangles can be constructed algebraically using braided monoidal categories. ________________________________________ From: homotopytypetheory@googlegroups.com [homotopytypetheory@googlegroups.com] on behalf of Michael Shulman [shulman@sandiego.edu] Sent: Friday, July 20, 2018 10:54 AM To: Urs Schreiber Cc: Homotopy Type Theory Subject: Re: [HoTT] What is knot in HOTT? It seems to me that especially if we want to construct *particular* knots, we would need the smooth reals to at least be a ring and probably to support trigonometric functions. On Fri, Jul 20, 2018 at 6:45 AM, 'Urs Schreiber' via Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com> wrote: >> Once we have the "smooth real numbers", wouldn't we just define S^1 >> and S^3 in terms of them as usual? Or are you saying that the problem >> is in characterizing the smooth reals inside differential cohesion? > > Yes. > > Possibly one could make progress by declaring shape to be homotopy > localization at some type A^1 of which we only demand that it be > homogeneous (as in Def. 4.8 in arxiv.org/abs/1806.05966) and then > focus attention on A^n-manifolds (as in Def. 7.1). > > One could maybe declare that a smooth n-sphere to be an A^n-manifold > whose shape is equivalent to Disc(S^n). Classically, this should work > away from dimensions in which there are exotic spheres, hence in > particular for the case n <= 3 of relevance in knot theory. > > Best wishes, > urs > > -- > 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. -- 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.

> It seems to me that especially if we want to construct *particular* > knots, we would need the smooth reals to at least be a ring and > probably to support trigonometric functions. One could require an isomorphism Disc(A) = R_{Cauchy} such that combined with the counit A --> Disc(A) = R_Cauchy this respects the homogeneous type structure on both sides (i.e the postulated one on the left, the canonical one given by addition on the right). To test such choices of axioms, it would be very helpful to have a concrete proposition in knot theory in mind, which one could aim for. Preferably some very simple proposition which is still of interest. Best, urs -- 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.

Gr, here I mean "flat" where I wrote "Disc", and the counit should go the other way around... On 7/20/18, Urs Schreiber <urs.schreiber@googlemail.com> wrote: >> It seems to me that especially if we want to construct *particular* >> knots, we would need the smooth reals to at least be a ring and >> probably to support trigonometric functions. > > One could require an isomorphism > > Disc(A) = R_{Cauchy} > > such that combined with the counit > > A --> Disc(A) = R_Cauchy > > this respects the homogeneous type structure on both sides (i.e the > postulated one on the left, the canonical one given by addition on the > right). > > To test such choices of axioms, it would be very helpful to have a > concrete proposition in knot theory in mind, which one could aim for. > Preferably some very simple proposition which is still of interest. > > Best, > urs > -- 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.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 --]

[-- Attachment #1: Type: text/plain, Size: 4485 bytes --] 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 <alizter@gmail.com> 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 > <https://groups.google.com/d/msgid/HomotopyTypeTheory/b886590f-c92b-493b-8751-9b0a342e9bdf%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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. [-- Attachment #2: Type: text/html, Size: 5731 bytes --]