Workshop on Homotopy Type Theory and Univalent Foundations of Mathematics

May 16 - 20, 2016, The Fields Institute

Location: Fields Institute, Room 230

Overview

Homotopy Type Theory is a new area of research, combining ideas from homotopy theory (a branch of topology) and dependent type theory (a formal system studied in mathematical logic and theoretical computer science). It is based on the realization that the logical notion of equality between two objects can carry more information beyond its truth value and as such may resemble the notion of homotopy between two continuous maps. The workshop will consist of mini-courses in the mornings and research-level talks (invited and contributed) in the afternoons. As such, it is meant as a venue for both the experts in the field and researchers from related areas interested in learning more about Homotopy Type Theory.

Welcome Reception

There will be a reception on Sunday evening, starting at 7pm, at The Prenup Pub, which is located at 191 College Street, a short walk from the Fields Institute.

Schedule

Monday, May 16th, 2016
09:00 to 10:15	Mini-course: Synthetic homotopy theory Michael Shulman, University of San Diego
10:15 to 10:45	Coffee Break
10:45 to 12:00	Mini-course: Computational Higher Type Theory Robert Harper, Carnegie Mellon University
12:00 to 14:00	Lunch
14:00 to 15:00	Homotopy Type Theory in Lean Jeremy Avigad, Carnegie Mellon University, Floris van Doorn, Carnegie Mellon University
15:00 to 15:40	The fourth homotopy group of the three-dimensional sphere Guillaume Brunerie, Université de Nice Sophia-Antipolis
15:40 to 16:10	Coffee Break
16:10 to 16:50	The Seifert-van Kampen Theorem in Homotopy Type Theory Kuen-Bang Hou (Favonia), Carnegie Mellon University
16:50 to 17:30	Projective spaces in synthetic homotopy theory Ulrik Buchholtz, Carnegie Mellon University

Tuesday, May 17th, 2016
09:00 to 10:15	Mini-course: Synthetic homotopy theory Michael Shulman, University of San Diego
10:15 to 10:45	Coffee Break
10:45 to 12:00	Mini-course: Computational Higher Type Theory Robert Harper, Carnegie Mellon University
12:00 to 14:00	Lunch
14:00 to 15:00	Towards a synthetic theory of (∞,1)-categories Emily Riehl, Johns Hopkins University
15:00 to 15:30	Coffee Break
15:30 to 16:10	Algebraic model structures on cubical sets Christian Sattler, University of Leeds
16:10 to 16:50	Complete Segal objects and univalent maps Nima Rasekh, University of Illinois at Urbana Champaign

Wednesday, May 18th, 2016
09:00 to 10:15	Mini-course: Homotopy-theoretic models of type theory Peter LeFanu Lumsdaine, Stockholm University
10:15 to 10:45	Coffee Break
10:45 to 12:00	Mini-course: Cubical Type Theory Dan Licata, Wesleyan University

Thursday, May 19th, 2016
09:00 to 10:15	Mini-course: Homotopy-theoretic models of type theory Peter LeFanu Lumsdaine, Stockholm University
10:15 to 10:45	Coffee Break
10:45 to 12:00	Mini-course: Cubical Type Theory Dan Licata, Wesleyan University
12:00 to 14:00	Lunch
14:00 to 15:00	Why does Homotopy Type Theory matter? Thorsten Altenkirch, University of Nottingham
15:00 to 15:30	Coffee Break
15:30 to 16:10	Cubical Type Theory: a constructive interpretation of the univalence axiom Anders Mörtberg, Institute for Advanced Study
16:10 to 16:50	Cubical Sets Axiomatised in the Internal Type Theory of a Topos Ian Orton, University of Cambridge
18:30 to 21:30	Banquet, Via Mercanti, 87 Elm St.

Friday, May 20th, 2016
09:00 to 10:00	Categorical structures in type theory, in type theory Benedikt Ahrens, INRIA Nantes
10:00 to 10:40	Reducing HITs to quotients Floris van Doorn, Carnegie Mellon University
10:40 to 11:10	Coffee Break
11:10 to 11:50	Non-Recursive Higher Inductive Types Nicolai Kraus, University of Nottingham
11:50 to 12:30	Induction and homotopy initiality for a class of 1-HITs Gabe Dijkstra, University of Nottingham
12:00 to 14:00	Lunch
14:00 to 15:00	Directedness in type theory Michael Warren, HRL Laboratories
15:00 to 15:40	Constructive set theory in Homotopy Type Theory Håkon Robbestad Gylterud, Stockholm University
15:40 to 16:10	Coffee Break
16:10 to 16:50	Topological models of dependent type theory Paige North, University of Cambridge
16:50 to 17:30	Localization at maps between omega-compact types via a small object argument in HoTT Egbert Rijke, Carnegie Mellon University

Location

Room 230, Fields Institute

Speakers

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 (INRIA Nantes)
        Thorsten Altenkirch (University of Nottingham)
        Jeremy Avigad (Carnegie Mellon University)
        Emily Riehl (Johns Hopkins University)
        Michael Warren (HRL Laboratories)

Program

The workshop will consist of mini-courses in the mornings and research-level talks (invited and contributed) in the afternoons. It will run from approximately 9am to 5pm, from Monday to Friday, except for Wednesday afternoon, in Room 230 of the Fields Institute. A one-page schedule is available at this link.

Registration

Registration is now closed as the event has reached capacity.

Applications for funding are no longer being accepted.

A banquet dinner will be held on Thursday, May 19 at Via Mercanti starting at 6:30pm. If you plan on attending, please sign-up at the Fields Institute reception desk by Tuesday, May 17 (even if you already registered online). The banquet will cost $65.33 per person (includes taxes and gratuities). Click here to preview the menu (pdf file).

Cancellation notice: There is a $15 administrative charge for Conference registration cancellations. No refunds will be made for registration cancellation requests received after May 8, 2016. Cancellation requests should be sent by e-mail to homotopy-type<at>fields.utoronto.ca. Please provide: 1. Registrant’s complete name 2. Event name and dates 3. Reason(s) for cancellation 4. Copy/record of registration confirmation or receipt, if paid for online at time of registration.

Resources for Visitors

The following link provides information on facilities and resources available to visiting members of the Fields Instittute:
http://www.fields.utoronto.ca/resources/for-visitors

Accommodation

Participants should make their own arrangements for accommodation, using the housing resources found at http://www.fields.utoronto.ca/resources/housing-resources

There are also student residences available at excellent rates:

New College: http://www.ncsummer.utoronto.ca/rates/

University College: http://www.uc.utoronto.ca/summer-housing#rates

Trinity College: http://web.trinity.utoronto.ca/prospective/residence-dining/summer-resid...

Massey College: http://www.masseycollege.ca/facilities/summer-rentals/

Registered Participants

Name	Affiliation
Benedikt Ahrens	INRIA Nantes
Kristian Alfsvåg	University of Bergen
Thorsten Altenkirch	University of Nottingham
Jeremy Avigad	Carnegie Mellon University
Kristine Bauer	University of Calgary
Gershom Bazerman	S&P Global Market Intelligence
Auke Booij	University of Birmingham
Simon Boulier	Inria-Ecole Mines Nantes
Jason Brennan	Western University
Christopher Brown	University of Arizona
Guillaume Brunerie	Université de Nice Sophia-Antipolis
Ulrik Buchholtz	Carnegie Mellon University
Tim Campion	University of Notre Dame
Paolo Capriotti	University of Nottingham
Jeffrey Carlson	University of São Paulo
Michael Ching	Amherst College
Sea Moon Cho	University of Pennsylvania
Vikraman Choudhury	Indiana University
Dan Christensen	Western University
Robin Cockett	University of Calgary
Ben Darwin	Mouse Imaging Centre, Sick Kids Hospital
Gabe Dijkstra	University of Nottingham
Christopher Dutchyn	University of Saskatchewan
Kirill Elagin	JetBrains, Inc. / St. Petersburg Academic University
Jacopo Emmenegger	Stockholms Universitet
Aras Ergus	University of Bonn
Sergio Estrada	University of Murcia
Kyle Ferendo	Amherst College
Andrés Fontalvo Orozco	Western University
Jérôme Fortier	University of Ottawa
Jonathan Gallagher	University of Calgary
Robert Graham	McGill University
Jacob Gross	University of Pittsburgh
Håkon Robbestad Gylterud	Stockholm University
Robert Harper	Carnegie Mellon University
Kuen-Bang Hou (Favonia)	Carnegie Mellon University
Ting Chen Leo Hsu	University of British Columbia
Valery Isaev	JetBrains, inc.
Rick Jardine	Western University
Joe Johnson	Mary Baldwin College
Michael Johnson	Macquarie University
Krzysztof Kapulkin	Western University
Atoosa Kasirzadeh	University of Toronto
Ryszard Kostecki	Perimeter Institute
Nicolai Kraus	University of Nottingham
Alexander Kuklev	JetBrains GmbH
Michael Lambert	Dalhousie University
Ellen Lehet	University of Notre Dame
Jean-Simon Lemay	University of Calgary
John Leo	Maana, Inc
Paul Lessard	University of Colorado Boulder
Gabriel Lewertowski	INRIA
Dan Licata	Wesleyan University
Rory Lucyshyn-Wright	Mount Allison University
Peter LeFanu Lumsdaine	Stockholm University
Ben MacAdam	University of Calgary
Cyprien Mangin	l'université Paris-Diderot
Jeremy Mann	University of Notre Dame
Christopher Mary
Weixi Ma	Computer Science
Nicholas Meadows	Western University
Edward Morehouse	Carnegie Mellon University
Anders Mörtberg	Institute for Advanced Study
Sean Moss	University of Cambridge
Chad Nester	University of Calgary
Paige North	University of Cambridge
Russell O'Connor
Mkrtich Ohanyan	Syracuse University
Cihan Okay	Western University
Ian Orton	University of Cambridge
Robert Paré	Dalhousie University
Fedor Part	JetBrains Inc
Stefano Piceghello	University of Bergen
Dan Plyukhin	University of Toronto
Dorette Pronk	Dalhousie University
Nima Rasekh	University of Illinois at Urbana Champaign
Robert Rennie	University of Illinois at Urbana-Champaign
Charles Rezk	University of Illinois
James Richardson	Western University
Emily Riehl	Johns Hopkins University
Egbert Rijke	Carnegie Mellon University
Mitchell Riley	Western University
Robert Rosebrugh	Mount Allison University
Robert Rose	Indiana University
Daniel Satanove
Genki Sato	Graduate School of Mathematical Sciences, the University of Tokyo
Christian Sattler	University of Leeds
Victor Savkov
Luis Nerio Scoccola	FCEyN, UBA (Universidad de Buenos Aires)
Henri Shahrouz	Disney Studio
Michael Shulman	University of San Diego
Yuri Sulyma	University of Texas at Austin
Karol Szumilo	Western University
Shiyam Thavandiran	Western University
Walter Tholen	York University
Dann Toliver
Taichi Uemura	Kyoto University
Jonathan Vandenburgh	University of Notre Dame
Floris van Doorn	Carnegie Mellon University
Marco Vergura	Western University
Jakob von Raumer	University of Nottingham
Andrew Warren	Carnegie Mellon University
Michael Warren	HRL Laboratories
Felix Wellen	Karlsruhe Institute of Technology
Charles Wells	Case Western Reserve University
Pal Zsamboki	Western University
Colin Zwanziger	Carnegie Mellon University

The Fields Institute for
Research in Mathematical Sciences

Workshop on Homotopy Type Theory and Univalent Foundations of Mathematics

Overview

Welcome Reception

Schedule

Location

Speakers

Program

Registration

Registered Participants

Organizing Committee

Quick Links

People and Contacts

Calendar and Events