Workshop on Homotopy Type Theory and Univalent Foundations, Fields Institute, May 16-20, 2016

[Chris Kapulkin]

Dear all,

This is a reminder about the Workshop on Homotopy Type Theory and
Univalent Foundations to be held at the Fields Institute in Toronto,
May 16-20, 2016. The workshop will consist of mini-courses on several
aspects of Homotopy Type Theory, as well as research talks, both
invited and contributed. The registration and abstract submission are
available at:

http://www.fields.utoronto.ca/programs/scientific/15-16/homotopy-type/

Limited financial support is available to cover participants' travel
and local expenses. Priority will be given to junior researchers and
those without other sources of funding. To be considered for funding,
please fill out the Funding Application Form which is a part of the
online registration.

Important dates:
* Funding application deadline: February 28, 2016.
* Contributed talk submission deadline: February 28, 2016.
* Registration deadline: May 2, 2016. (Early registration is
appreciated, to help us in our planning.)

Program:

Mini-courses

Robert Harper (Carnegie Mellon University): Computational Higher Type Theory
Daniel R. Licata (Wesleyan University): Cubical Type Theory
Peter LeFanu Lumsdaine (Stockholm University): Homotopy-theoretic
models of type theory
Michael Shulman (University of San Diego): Synthetic Homotopy Theory

Invited speakers

Benedikt Ahrens (IAS, Princeton)
Thorsten Altenkirch (University of Nottingham)
Jeremy Avigad (Carnegie Mellon University)
Emily Riehl (Johns Hopkins University)
Michael Warren (HRL Laboratories)

We are looking forward to seeing you in Toronto!

Organizers: Dan Christensen, Rick Jardine, Chris Kapulkin

[Mark Farrell]

Hi,

I have a few general questions about the workshop in the spring:

- How will the mini-courses be structured? Being called mini-courses, does that imply participants will be given exercises to do, possibly even brainpicked about open problems, etc.?
- What will be covered on the more computing-related side of matters? For the computational higher type theory mini-course, will that have something to do with computational type theory,
as in the "richer" analogue of formal type theory seen in proof development systems like NuPRL and JonPRL? Or, does it mean computational, in the sense of e.g. formulating an extension to
formal type theory with a computational intepretation of univalence? I've inquired with another person already a bit about the cubical type theory course, but I guess just to throw the same question
out there, what will the cubical type theory workshop cover? Will it cover moreso the theory behind cubical type theories, or moreso showcase how to use the current state-of-the-art cubical type theory proof checker,
by e.g. illustrating developed examples of the proof that the fundamental group of the circle is the integers, the proof that the torus is the product of two circles, the construction of the Hopf fibration, etc.?
- I'm currently not too familiar with Lumsdaine's line of research, but by homotopy-theoretic models of type theory, does that mean, e.g. approaching the problem of finding models of some variant/extension of formal type theory in infinity-topoi?
- What will be addressed on the synthetic homotopy theory side of matters? What is the state-of-the-art in that regard, and where is there opportunity to go from there? As of now, it seems like Evan Cavallo's thesis on synthetic cohomology in homotopy type theory is the most recent (largest) completed body of work on the matter? Aside from that, are Mike Shulman's notes on spectral sequences in higher type theory, Brunerie's work on the proof that the fourth homotopy group of the three-sphere is Z/2Z, and Buchholtz's work on the construction of the super-Hopf fibration the 'bleeding edge' of work that's being done in synthetic homotopy theory? Will the synthetic homotopy workshop teach/address these developments in detail? In general, what will this particular workshop cover as well?
- To what extent will the workshops try to be in harmony with each other (e.g. the synthetic homotopy workshop making use of state-of-the-art ideas from the cubical/higher type theory research side of matters?)
- I've noticed Emily Riehl is an invited speaker. Her book on 'categorical homotopy theory' looks quite interesting to me, but is definitely beyond my level of knowledge and ability. Is that fine? Like, to what extent are these invited talks supposed to spark collaboration and creativity beyond the direct scope of the mini-courses?
- Lastly, generally speaking, to what extent is this workshop appropriate to an amateur (like me, I suppose), largely taking an interest in this area of research in my spare time, without, strictly speaking, much formal training on either side of matters? Like, who is/are the specific target audience(s) of this workshop? How large do you think the audience will be? Do you anticipate there will be other people with no particular formal background, who are just interested in HoTT, there?

Anyways, just throwing these questions I have on my mind out there, I suppose. Would be happy if anyone on the mailing list, whether it be the conference organizers or individuals otherwise, wants to chime in.

Thanks,

Mark.

[Chris Kapulkin]

Dear Mark,

On behalf of the organizers, I'd like to thank you for your interest in the workshop. Regarding your questions, it's very difficult for us, the organizers, to guess what would be covered by each speaker. We are grateful that they accepted our invitations and do not intend to tell them what they should talk about or which aspects of their minicourse topics they should focus on. Regarding the necessary background, it's again hard to predict the level of all talks. I think some familiarity with (homotopy) type theory will be required, so it's a good idea to familiarize yourself with the first few chapters of the HoTT Book beforehand.

Closer to the date, we will ask the invited speakers for abstracts of their talks and will then post them on the website. That may help answer some of your questions.

I'd be happy to answer any other questions you may have, but it may be a good idea to take this discussion off the list.

Best regards,

Chris Kapulkin

--
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 HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.