Skip to main content

Workshop on Homotopy Type Theory

Posted in
Michael Batanin, Christian Blohmann, Ralph Kaufmann, Martin Markl
Wed, 10/02/2016 - 08:00 - Sun, 14/02/2016 - 22:00
MPIM Lecture Hall



The workshop will give the participants the chance to discuss of current problems in areas of active research in homotopy type theory. Each day will start with a lecture series by Vladimir Voevodsky on "Dependent Type Theory", followed by open seminars in which workshop participants can give short presentations on their research.

The lecture series by Vladimir Voevodsky was recorded and can be found here .

Workshop co-ordinator:

Richard Garner (Macquarie University)

Preliminary list of participants

Ahrens, Benedikt (Institute for Advanced Study )
Awodey, Steve (Carnegie Mellon University )
Bakovic, Igor (Croatia)
Bauer, Andej (University of Ljubljana)
Berger, Clemens (Université de Nice - Sophia Antipolis)
Blanc, David (University of Haifa )
Bordg, Anthony (Charles University Prague)
Breen, Lawrence (Université Paris Nord 13 )
Brunerie, Guillaume (École normale supérieure Paris)
Buchholtz, Ulrik (Carnegie Mellon University )
Cartier, Pierre (IHES)
Chapoton, Frederic (Université de Strasbourg)
Coquand, Thierry (Department of Computer Science and Engineering)
Curien, Pierre-Louis (Université Paris Diderot )
David, Sabonis (TU Munich)
Dotsenko, Vladimir (Trinity College Cambridge )
Doubek, Martin (Charles University Prague )
Durov, Nicolai (V. A. Steklov Institute of Mathematics )
Escardo, Martin (University of Birmingham)
Finster, Eric (LIX, École Polytechnique)
Fiore, Marcelo (University of Cambridge )
Fresse, Benoit (Université de Lille 1 )
Galvez Carrillo, Maria Immaculada (Universitat Politècnica de Catalunya)
Garner, Richard (Macquarie University )
Grayson, Dan (University of Illinois at Urbana-Champaign)
Haselwarter, Philipp (U.F.R. Mathématiques)
Hinich, Vladimir (University of Haifa )
Hofstra, Pieter Jan  (University of Ottawa )
Huber, Simon (Chalmers University of Technology)
Jaun, Lukas (Institute of Computer Science)
Joyal, André (Université du Quebec à Montréal )
Jurco, Branislav (Charles University )
Kapulkin, Chris (The University of Western Ontario )
Kassel, Christian (Université de Strasbourg et CNRS)
Kock, Joachim (Universitat Autònoma de Barcelona )
Le Grignou, Brice (Université de Nice - Sophia Antipolis)
Livernet, Muriel (Université Paris Diderot)
Lumsdaine, Peter (Stockholm University)
Makkai, Michael (McGill University)
Maltsiniots, Georges (Université Paris Diderot)
Martin-Löf, Per (Stockholm University)
Moerdijk, Ieke (Utrecht University )
Neeman, Amnon (The Australian National University )
Newstead, Clive (Carnegie Mellon University)
North, Paige (University of Cambridge)
Palmgren, Erik (Stockholm University)
Rijke, Egbert (Carnegie Mellon University)
Robayo Mesa, Jaime Andrés (Universidad Nacional de Colombia)
Ronco, Maria Ofelia (Universidad de Talca )
Salvatore, Paolo (Universit a di Roma Tor Vergata )
Sattler, Christian (University of Leeds )
Schreiber, Urs (Czech Academy of Sciences )
Shin, Heayong (Department of Mathematics)
Sinha, Dev Parakash (University of Oregon )
Sojakova, Kristina (Carnegie Mellon University)
Spitters, Bas (Aarhus University)
Streicher, Thomas (Technische Universität Darmstadt )
Szawiel, Stanisław (University of Warsaw)
Tonks, Andrew (University of Leicester)
Trlifaj, Jan (Charles University)
Vallette, Bruno (Université Paris Nord 13 )
van den Berg, Benno (University of Amsterdam )
Verchinine, Vladimir (Université Montpellier II )
Voevodsky, Vladimir (Institute for Advanced Study )
von Glehn, Tamara (University of Cambridge)
Weber, Mark (Macquarie University )
Wellen, Felix (Karlsruhe Institute of Technology)
Zawadowski, Marek (University of Warsaw)


Workshop on Homotopy Type Theory February 10 - 14, 2016






Lunch break

Lunch break

Lunch break

Lunch break

Lunch break

Chris Kapulkin
Benno van den Berg
Bas Spitters
Egbert Rijke
Dan Grayson




Simon Hubert
Clemens Berger
Ulrik Buchholtz
Bas Spitters
Eric Finster
Peter Lumsdaine
Thomas Streicher
Andrej Bauer
Peter Lumsdaine

Lectures by Vladimir Voevodsky: "Dependent Type Theories"

Abstract: Modern dependent type theories exist mostly in the form of computer programs. As such they are objects of the physical reality more than they are objects of the mathematical one. For three decades the world of type theories was relatively calm - innovation was largely occurring in the layers of programming above the type theories leading to proof assistants with more and more sophisticated systems for notation, implicit arguments and tactics.

The discovery of the univalent models led to the addition of new features to the existing type theories as well as to the development of entirely new ones such as cubicaltt. Eventually, these new type theories will become the cores of proof assistants with much more convenient than before environments for formal verification of mathematical arguments.

It is clear that the only way to ensure that these new proof assistants are reliable - that any proof of “false” in such a proof assistant can be mechanically transformed into a proof of “false” in one of the “consistency standards”, is to have a system where a new proof assistant has to be formally certified using an already certified proof assistant against an already certified formal system before it can become accepted as a reliable tool in pure mathematics.

The strongest consistency standard available in pure mathematics is ZFC. This means that as a prerequisite  for such a certification system we need to have a mathematical theory of dependent type theories that can be formalized in ZFC. At the moment only fragments of this future theory exist. I will give an introduction to my vision of the theory by describing these fragments and pointing out the gaps.

Organizing committee

Michael Batanin (Macquarie University)
Christian Blohmann (MPIM Bonn)
Ralph Kaufmann (Purdue University)
Martin Markl (Czech Academy of Sciences)


To register please use this registration webform. There is no registration fee. For any further inquiries please send an email to

Hotel reservations

If you would like us to make a hotel reservation for you, please state this on the registration webform. We can only honor requests for hotel reservations made by January 31,  2016. If you would like to make a hotel reservation by yourself you will find a list of hotels here.


File htt2016_MPIM_A3.pdf3.67 MB
© MPI f. Mathematik, Bonn Impressum & Datenschutz
-A A +A