Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

February 8, 2018

Homotopy Type Theory Electronic Seminar

Posted by John Baez

What a great idea! A seminar on homotopy type theory, with talks by top experts, available to everyone with internet connection!

Dear all,

We are pleased to announce the start of the Homotopy Type Theory Electronic Seminar Talks, a series of online talks by the leading experts in Homotopy Type Theory. The Seminar is open to all, although knowledge of the main concepts of HoTT will be assumed.

The Seminar will meet on alternating Thursdays at 11:30 AM Eastern, starting on February 15. We will be using Zoom for the talks. Zoom is similar to Skype, and provides software for all common platforms and devices.

For more details, including schedule of talks and the information on how to attend the meetings, please see:

http://uwo.ca/math/faculty/kapulkin/seminars/hottest.html

The inaugural talks will be given by:

February 15 Peter LeFanu Lumsdaine (Stockholm University) Inverse diagram models of type theory

March 1 Emily Riehl (Johns Hopkins University) The synthetic theory of infinity-categories vs the synthetic theory of infinity-categories

March 15 Carlo Angiuli (Carnegie Mellon University) Computational semantics of Cartesian cubical type theory

We are looking forward to seeing you all there!

Best wishes, Dan Christensen and Chris Kapulkin

Posted at February 8, 2018 5:11 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3017



18 Comments & 0 Trackbacks

Re: Homotopy Type Theory Electronic Seminar

Is Emily Riehl’s talk supposed to be groupoids vs categories?

Posted by: Max S New on February 8, 2018 11:26 AM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

One of the organizers, Chris Kapulkin, responds:

Haha, I asked her myself if she’s sure about the title before posting it. (-:

But yeah, the talk is aimed to be a comparison between her joint work with Dominic Verity and Mike Shulman. Two different synthetic theories of infinity-categories.

Posted by: John Baez on February 8, 2018 3:59 PM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

Ah, that was my guess about what she meant. Presumably the abstract will make it clear.

Posted by: Mike Shulman on February 8, 2018 6:11 PM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

The idea for this talk was inspired by the last few minutes of Mike’s talk at the Joint Mathematics Meetings on homotopical trinitarianism. Specifically, in the discussion “from the present to the future” Mike outlines trinitarian success stories, where a mathematical definition leads to the study of the category of such objects, which leads to a type theory modeled on the internal language of such categories, which leads to a synthetic approach to the original mathematical object of interest.

For a long time now I’ve been interesting in streamlining the development of the theory of (∞,1)(\infty,1)-categories - frequently nicknamed ∞\infty-categories. I’ve now been involved with two research projects that go some way to achieving this: one (joint with Dominic Verity) developed in classical categorical foundations and one (joint with Mike Shulman) developed in an augmented version of homotopy type theory.

I thought it would be interesting for other researchers who might be motivated to adopt a similar strategy to study their particular objects of interest to step back and compare the merits and drawbacks of each approach. But I haven’t written the talk yet, so beyond this, I really have no idea what I’ll end up saying!

Posted by: Emily Riehl on February 11, 2018 5:05 PM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

Is there more to be added at nLab: computational trinitarianism as to why moving about these triangles (in either direction or both) can work so well?

This case

a mathematical definition leads to the study of the category of such objects, which leads to a type theory modeled on the internal language of such categories, which leads to a synthetic approach to the original mathematical object of interest,

sounds like the nLab: microcosm principle might come into play, no?

Posted by: David Corfield on February 13, 2018 10:26 AM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

The microcosm principle does crop up in a related place, namely the abstract study of modal type theories, where the “mode theory” determining a particular modal type theory is itself a “2-type theory”. The corresponding semantic picture is a little different from the usual microcosm situation, though, in that instead of considering internal widgets in a 2-widget, so far it has seemed better to consider widgets fibered over a 2-widget.

Posted by: Mike Shulman on February 13, 2018 11:56 AM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

It would be one thing if passing around the triangle were just a matter of finding analogues along equivalences, but quite another if something ‘ampliative’ is going on.

(Ampliative inference is usually taken as inference whose conclusion goes beyond the premises.)

I’ve been playing a little with the idea that the modes of inference characterised by Charles Peirce – deduction, induction, abduction (the latter two ampliative) – are just so many ways of completing a triangle of arrows.

So deduction resembles composing arrows; induction resembles extension (especially along a mono); abduction/explanation resembles lifting (especially along an epi).

Could your passages around the triangle be seen even vaguely in that light?

Posted by: David Corfield on February 14, 2018 11:32 AM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

Hmm, I’m not sure. Maybe.

Posted by: Mike Shulman on February 18, 2018 6:35 AM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

Will there be recordings of this seminars? Sadly I’ll not be able to attend them.

Posted by: Sebas on February 10, 2018 3:48 PM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

We’ll be recording the talks, and then each speaker will get to decide whether we post the recording publicly or delete it.

On another note, to avoid having participants be disappointed, I wanted to make it clear that we’ve told the speakers to assume background in homotopy type theory, similar to what is in the HoTT book.

Posted by: Dan Christensen on February 10, 2018 9:01 PM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

Thanks for making that clear! However, while the HoTT Book is an obvious “reference point” for background, it’s somewhat lopsided in its representation of the field in that it’s entirely about doing mathematics in HoTT, and includes practically nothing about semantics or metatheory. Will every speaker who wants to talk about semantics have to start at square one with the definition of a comprehension category etc.? Or could different talks require different backgrounds?

Posted by: Mike Shulman on February 10, 2018 11:56 PM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

“similar to what is in the HoTT book” is just a very rough way to give an indication that some background is assumed. A speaker might use their abstract to give a more precise indication of the background that they will (or will not) assume.

Posted by: Dan Christensen on February 11, 2018 8:09 PM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

By the way, the title of this blog post is missing the last word in the name of the seminar series: Homotopy Type Theory Electronic Seminar Talks. I gather that this produce a better acronym.

Posted by: Mike Shulman on February 14, 2018 5:55 PM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

I’ve never heard of Zoom before. Who are they?

The FF/Chrome extensions needs access to my google account. That’s a bit too much for me. Is there another way? Zoom also provides a .deb file for linux, but it’s not in Ubuntu, so not vetted by anyone that I trust, as far as I can see. Am I overlooking something?

Posted by: Bas Spitters on February 15, 2018 1:19 PM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

Zoom is widely used for large meetings, including several other mathematics seminars. It has better quality that Skype in my tests, and can host hundreds of participants. I used the .deb in my Ubuntu installation, and did not have to link to a Google account. You don’t even need to sign up for a Zoom account to participate.

By the way, neither the Skype binary nor the Google Hangout plug-in are vetted by third parties either.

Posted by: Dan Christensen on February 16, 2018 3:10 AM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

Apparently, their app has been vetted on android and I guess by apple too, but the list of permissions they ask is long. E.g.

  • add or modify calendar events and send email to guests without owners’ knowledge

It’s been a long time since I’ve installed random .debs on my computer (skype is in Ubuntu). I’m not criticizing, just trying to make an informed decision. WebRTC and Firefox Hello was supposed to solve this mess.

Posted by: Bas Spitters on February 16, 2018 10:36 AM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

I share your concerns about this issue and I think it’s good to raise these points. I of course would prefer an open source option, but the management features that Zoom provides go far beyond what is available in other options. I started with Zoom because for connecting one-on-one with someone in China, the quality is much better than Skype, and we chose it for the HoTTEST seminar because it comes highly recommended from people organizing similar seminars.

By the way, I don’t think Skype is in Ubuntu. An older version of Skype (which doesn’t work anymore) was in the “partners” repository, but now you have to install the snap. In either case, Ubuntu has no access to the source code to vet this. Similarly, many of us run Google Chrome, which is not vetted in any way.

Posted by: Dan Christensen on February 16, 2018 2:02 PM | Permalink | Reply to this

Re: Homotopy Type Theory Electronic Seminar

The first talk in this seminar went very well. Peter Lumsdaine gave a delightful overview of recent work with Chris Kapulkin, and there were around 80 people attending (some in groups sharing a connection). As we had hoped, there were good questions and discussion during and after the talk.

Peter has agreed to have the video posted, and when this is done, it will be linked to from the seminar web page.

Posted by: Dan Christensen on February 16, 2018 2:43 PM | Permalink | Reply to this

Post a New Comment