Re: [HoTT] What is knot in HOTT?

["'Urs Schreiber' via Homotopy Type Theory" <HomotopyTypeTheory@googlegroups.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.