Re: [HoTT] What is knot in HOTT?

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

Gr, here I mean "flat" where I wrote "Disc", and the counit should go
the other way around...

On 7/20/18, Urs Schreiber <urs.schreiber@googlemail.com> wrote:
>> It seems to me that especially if we want to construct *particular*
>> knots, we would need the smooth reals to at least be a ring and
>> probably to support trigonometric functions.
>
> One could require an isomorphism
>
>  Disc(A) = R_{Cauchy}
>
> such that combined with the counit
>
>  A --> Disc(A) = R_Cauchy
>
> this respects the homogeneous type structure on both sides (i.e the
> postulated one on the left, the canonical one given by addition on the
> right).
>
> To test such choices of axioms, it would be very helpful to have a
> concrete proposition in knot theory in mind, which one could aim for.
> Preferably some very simple proposition which is still of interest.
>
> Best,
> 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.