```
From: "'Urs Schreiber' via Homotopy Type Theory" <HomotopyTypeTheory@googlegroups.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] What is knot in HOTT?
Date: Fri, 20 Jul 2018 14:27:39 +0400
Message-ID: <CA+KbugetwD6XckDi3TnULMHsf9K_w0=07DTXCBfd7V+2pgdjNQ@mail.gmail.com> (raw)
In-Reply-To: <CAOvivQykUDH9h4iJ1bz1uy1Uc7VLoRFEV4HyferLY+qbrNXORw@mail.gmail.com>
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.
```

next prev parent reply other threads:[~2018-07-20 10:27 UTC|newest]Thread overview:16+ messages / expand[flat|nested] mbox.gz Atom feed top 2018-07-19 5:18 José Manuel Rodriguez Caballero 2018-07-19 5:45 ` Egbert Rijke 2018-07-19 8:55 ` Ali Caglayan 2018-07-19 15:31 ` Michael Shulman2018-07-20 10:27 ` 'Urs Schreiber' via Homotopy Type Theory [this message]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

Reply instructions:You may reply publicly to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the--to,--cc, and--in-reply-toswitches of git-send-email(1): git send-email \ --in-reply-to='CA+KbugetwD6XckDi3TnULMHsf9K_w0=07DTXCBfd7V+2pgdjNQ@mail.gmail.com' \ --to=homotopytypetheory@googlegroups.com \ --cc=urs.schreiber@googlemail.com \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting theIn-Reply-Toheader via mailto: links, try the mailto: link

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 \ homotopytypetheory@googlegroups.com public-inbox-index hott Example config snippet for mirrors. Newsgroup available over NNTP: nntp://inbox.vuxu.org/vuxu.archive.hott AGPL code for this site: git clone https://public-inbox.org/public-inbox.git