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 <email@example.com> 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 HomotopyTypeTheoryfirstname.lastname@example.org. For more options, visit https://groups.google.com/d/optout.
next prev parent reply index 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 Shulman 2018-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-to switches of git-send-email(1): git send-email \ --in-reply-to='CA+KbugetwD6XckDi3TnULMHsf9K_w0=07DTXCBfd7V+2pgdjNQ@mail.gmail.com' \ --email@example.com \ --firstname.lastname@example.org \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting the In-Reply-To header via mailto: links, try the mailto: link
Discussion of Homotopy Type Theory and Univalent Foundations Archives are clonable: git clone --mirror http://inbox.vuxu.org/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