Discussion of Homotopy Type Theory and Univalent Foundations
help / color / mirror / Atom feed
* [HoTT] What is knot in HOTT?
@ 2018-07-19  5:18 José Manuel Rodriguez Caballero
2018-07-19  5:45 ` Egbert Rijke
From: José Manuel Rodriguez Caballero @ 2018-07-19  5:18 UTC (permalink / raw)
To: HomotopyTypeTheory

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

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.

[-- Attachment #2: Type: text/html, Size: 778 bytes --]

• * Re: [HoTT] What is knot in HOTT?
2018-07-19  5:18 [HoTT] What is knot in HOTT? José Manuel Rodriguez Caballero
@ 2018-07-19  5:45 ` Egbert Rijke
2018-07-19  8:55   ` Ali Caglayan
2018-07-19 17:56   ` Daniel R. Grayson
0 siblings, 2 replies; 16+ messages in thread
From: Egbert Rijke @ 2018-07-19  5:45 UTC (permalink / raw)
To: José Manuel Rodriguez Caballero; +Cc: Homotopy Type Theory

[-- 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?
>
>
> 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
> 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.

[-- Attachment #2: Type: text/html, Size: 3732 bytes --]

• * Re: [HoTT] What is knot in HOTT?
2018-07-19  5:45 ` Egbert Rijke
@ 2018-07-19  8:55   ` Ali Caglayan
2018-07-19 15:31     ` Michael Shulman
2019-11-20 19:13     ` Ali Caglayan
2018-07-19 17:56   ` Daniel R. Grayson
1 sibling, 2 replies; 16+ messages in thread
From: Ali Caglayan @ 2018-07-19  8:55 UTC (permalink / raw)
To: Homotopy Type Theory

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

--
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.

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

• * Re: [HoTT] What is knot in HOTT?
2018-07-19  8:55   ` Ali Caglayan
@ 2018-07-19 15:31     ` Michael Shulman
2018-07-20 10:27       ` 'Urs Schreiber' via Homotopy Type Theory
2019-11-20 19:13     ` Ali Caglayan
From: Michael Shulman @ 2018-07-19 15:31 UTC (permalink / raw)
To: Ali Caglayan; +Cc: Homotopy Type Theory

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
>
> --
> 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
> 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.

• * Re: [HoTT] What is knot in HOTT?
2018-07-19 15:31     ` Michael Shulman
@ 2018-07-20 10:27       ` 'Urs Schreiber' via Homotopy Type Theory
2018-07-20 13:32         ` Michael Shulman
From: 'Urs Schreiber' via Homotopy Type Theory @ 2018-07-20 10:27 UTC (permalink / raw)
To: Homotopy Type Theory

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.

• * Re: [HoTT] What is knot in HOTT?
2018-07-20 10:27       ` 'Urs Schreiber' via Homotopy Type Theory
@ 2018-07-20 13:32         ` Michael Shulman
2018-07-20 13:45           ` 'Urs Schreiber' via Homotopy Type Theory
From: Michael Shulman @ 2018-07-20 13:32 UTC (permalink / raw)
To: Urs Schreiber; +Cc: Homotopy Type Theory

On Fri, Jul 20, 2018 at 3:27 AM, 'Urs Schreiber' via Homotopy Type
> 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.

• * Re: [HoTT] What is knot in HOTT?
2018-07-20 13:32         ` Michael Shulman
@ 2018-07-20 13:45           ` 'Urs Schreiber' via Homotopy Type Theory
2018-07-20 14:54             ` Michael Shulman
From: 'Urs Schreiber' via Homotopy Type Theory @ 2018-07-20 13:45 UTC (permalink / raw)
To: Michael Shulman; +Cc: Homotopy Type Theory

> 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.

• * Re: [HoTT] What is knot in HOTT?
2018-07-20 13:45           ` 'Urs Schreiber' via Homotopy Type Theory
@ 2018-07-20 14:54             ` Michael Shulman
2018-07-20 15:17               ` Joyal, André
2018-07-20 16:40               ` 'Urs Schreiber' via Homotopy Type Theory
0 siblings, 2 replies; 16+ messages in thread
From: Michael Shulman @ 2018-07-20 14:54 UTC (permalink / raw)
To: Urs Schreiber; +Cc: Homotopy Type Theory

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
>> 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.

• * RE: [HoTT] What is knot in HOTT?
2018-07-20 14:54             ` Michael Shulman
@ 2018-07-20 15:17               ` Joyal, André
2018-07-20 16:40               ` 'Urs Schreiber' via Homotopy Type Theory
1 sibling, 0 replies; 16+ messages in thread
From: Joyal, André @ 2018-07-20 15:17 UTC (permalink / raw)
To: Michael Shulman, Urs Schreiber; +Cc: Homotopy Type Theory

Of course, braids, knots and tangles can be constructed algebraically
using braided monoidal categories.

________________________________________
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
>> 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.

--
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.

• * Re: [HoTT] What is knot in HOTT?
2018-07-20 14:54             ` Michael Shulman
2018-07-20 15:17               ` Joyal, André
@ 2018-07-20 16:40               ` 'Urs Schreiber' via Homotopy Type Theory
2018-07-20 16:42                 ` 'Urs Schreiber' via Homotopy Type Theory
From: 'Urs Schreiber' via Homotopy Type Theory @ 2018-07-20 16:40 UTC (permalink / raw)
To: Michael Shulman; +Cc: Homotopy Type Theory

> 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.

• * Re: [HoTT] What is knot in HOTT?
2018-07-20 16:40               ` 'Urs Schreiber' via Homotopy Type Theory
@ 2018-07-20 16:42                 ` 'Urs Schreiber' via Homotopy Type Theory
0 siblings, 0 replies; 16+ messages in thread
From: 'Urs Schreiber' via Homotopy Type Theory @ 2018-07-20 16:42 UTC (permalink / raw)
To: Michael Shulman; +Cc: Homotopy Type Theory

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.

• * Re: [HoTT] What is knot in HOTT?
2018-07-19  8:55   ` Ali Caglayan
2018-07-19 15:31     ` Michael Shulman
@ 2019-11-20 19:13     ` Ali Caglayan
2019-11-20 21:02       ` andré hirschowitz
From: Ali Caglayan @ 2019-11-20 19:13 UTC (permalink / raw)
To: Homotopy Type Theory

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

--
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.

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

• * Re: [HoTT] What is knot in HOTT?
2019-11-20 19:13     ` Ali Caglayan
@ 2019-11-20 21:02       ` andré hirschowitz
0 siblings, 0 replies; 16+ messages in thread
From: andré hirschowitz @ 2019-11-20 21:02 UTC (permalink / raw)
To: Ali Caglayan; +Cc: Homotopy Type Theory

[-- 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
>>
> --
> 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
> To view this discussion on the web visit
> .
>

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

• * Re: [HoTT] What is knot in HOTT?
2018-07-19  5:45 ` Egbert Rijke
2018-07-19  8:55   ` Ali Caglayan
@ 2018-07-19 17:56   ` Daniel R. Grayson
2018-07-19 18:38     ` Egbert Rijke
From: Daniel R. Grayson @ 2018-07-19 17:56 UTC (permalink / raw)
To: Homotopy Type Theory

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

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

• * Re: [HoTT] What is knot in HOTT?
2018-07-19 17:56   ` Daniel R. Grayson
@ 2018-07-19 18:38     ` Egbert Rijke
2018-07-19 20:07       ` José Manuel Rodriguez Caballero
From: Egbert Rijke @ 2018-07-19 18:38 UTC (permalink / raw)
To: Daniel R. Grayson; +Cc: Homotopy Type Theory

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

[-- Attachment #2: Type: text/html, Size: 3094 bytes --]

• * Re: [HoTT] What is knot in HOTT?
2018-07-19 18:38     ` Egbert Rijke
@ 2018-07-19 20:07       ` José Manuel Rodriguez Caballero
0 siblings, 0 replies; 16+ messages in thread
From: José Manuel Rodriguez Caballero @ 2018-07-19 20:07 UTC (permalink / raw)
To: HomotopyTypeTheory

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

[-- Attachment #2: Type: text/html, Size: 4468 bytes --]

2018-07-19  5:18 [HoTT] What is knot in HOTT? José Manuel Rodriguez Caballero
2018-07-19  5:45 ` Egbert Rijke
2018-07-19  8:55   ` Ali Caglayan
2018-07-19 15:31     ` Michael Shulman
2018-07-20 10:27       ` 'Urs Schreiber' via Homotopy Type Theory
2018-07-20 13:32         ` Michael Shulman
2018-07-20 13:45           ` 'Urs Schreiber' via Homotopy Type Theory
2018-07-20 14:54             ` Michael Shulman
2018-07-20 15:17               ` Joyal, André
2018-07-20 16:40               ` 'Urs Schreiber' via Homotopy Type Theory
2018-07-20 16:42                 ` 'Urs Schreiber' via Homotopy Type Theory
2019-11-20 19:13     ` Ali Caglayan
2019-11-20 21:02       ` andré hirschowitz
2018-07-19 17:56   ` Daniel R. Grayson
2018-07-19 18:38     ` Egbert Rijke
2018-07-19 20:07       ` José Manuel Rodriguez Caballero

Discussion of Homotopy Type Theory and Univalent Foundations

This inbox may be cloned and mirrored by anyone:

git clone --mirror http://inbox.vuxu.org/hott

# If you have public-inbox 1.1+ installed, you may
# initialize and index your mirror using the following commands:
public-inbox-init -V1 hott hott/ http://inbox.vuxu.org/hott \