The Department of Mathematics

Middlesex College

London, ON

Canada, N6A 5B7

Tel: 519.661.3639

Fax: 519.661.3610

Undergraduate inquiries:

math-inquiry@uwo.ca

Graduate inquiries:

math-grad-program@uwo.ca

All other inquiries:

mathdept@uwo.ca

Homotopy Type Theory Electronic Seminar Talks is a series of research talks by leading experts in Homotopy Type Theory. The seminar is open to all, although **familiarity with Homotopy Type Theory will be assumed**. To attend a talk, please follow the instructions below.

**Time:**alternate Thursdays at 11:30 AM Eastern.**Mailing list:**HoTT Electronic Seminar Talks (for updates).**Google Calendar:**link.**Organizers:**Dan Christensen and Chris Kapulkin.

We are using Zoom for the talks. Zoom is similar to Skype, and provides software for all common platforms and devices. Please install the software and make at least one test call before joining a talk. Please join the meeting a few minutes before the scheduled start time and mute your microphone when not asking a question. To join please follow the link:

We encourage attendees from the same institution to attend using one connection.

Electronic seminars are becoming more common in mathematics and you may be interested in attending some of them:

- Electronic Computational Homotopy Theory Seminar by Dan Isaksen
- Electronic Mathematics Education Seminar by Haynes Miller and Lourdes Alemán

Date |
Speaker |
Talk information |

March 1 |
Johns Hopkins University |
Ideal background: some familiarity with notions of a (ordinary strict 1-)category, functor, natural transformation, and the definition of an adjunction involving a unit and a counit (just look these up on wikipedia). Plus standard type theory syntax and the intuitions from the Curry-Howard-Voevodsky correspondence. I’ll be talking about (∞,1)-categories but won’t assume familiarity with them. |

March 15 |
Carnegie Mellon University |
Abstract: TBA |

Date |
Speaker |
Talk information |

February 15 |
Stockholm University |
For the case of intensional type theory, this becomes a little tricky. Since most logical constructors (e.g. Σ-types, Id-types) are not provably strictly functorial, it is difficult to lift them from structure on C to structure in C However, in case I is an I will discuss the construction of these models (and slightly more general The work of this talk is joint work with Chris Kapulkin, in arXiv:1610.00037 and a forthcoming companion article; see also Shulman arXiv:1203.3253 for a closely related construction. A basic familiarity with categorical models of type theory will be helpful, i.e. categories with attributes or similar; see here for an introductory overview of these. |