Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
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.

  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 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' \
    --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 the In-Reply-To header
  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