Re: [HoTT] What is knot in HOTT?

["'Urs Schreiber' via Homotopy Type Theory" <HomotopyTypeTheory@googlegroups.com>]

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