>
> Michael Shulman wrote:
>
what "algebraic" information it uses as input.


In the case of the Hilbert scheme of n points on X, the information comes
from the n-th symmetric power of X: https://arxiv.org/pdf/math/0304302.pdf

So, the input are X as an infinite-groupoid and the natural number n. The
output is the Hilbert scheme of n points on X as an infinite groupoid. I do
not know if there is some nice functoriality in this process which could be
expressed in HoTT in a natural way.  There are more results about the
Hilbert schemes it in Goettsche's homepage: http://users.ictp.it/~gottsche/

Kind Regards,
José M.


El lun., 24 sept. 2018 a las 19:59, Steve Awodey (<awodey@cmu.edu>)
escribió:

> > On Sep 24, 2018, at 6:30 PM, Ali Caglayan <alizter@gmail.com> wrote:
> >
> > However I don't want to discourage you. One possible solution is
> (differential?) cohesive homotopy type theory (which is at the moment even
> more undeveloped). This may allow you to talk about manifolds and their
> structure "synthetically" which would allow for definitions of de Rham
> cohomology and possibly with care allow you to talk about hilbert schemes
> of some torus. Pessemistically I would add that it would be at least 10
> years before any of this is considered.
>
> just for perspective:
>
> - 10 years ago we had the (higher) homotopy group(oid)s, and not much more.
> - 5 years ago the HoTT book was just finished.
> - 1 year ago the Serre spectral sequence was finished.
>
> things are moving pretty fast - I would not be so pessimistic.
>
> Steve
>
> --
> 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.
>

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