2019 Midwest Homotopy Type Theory Seminar

Essential Information

  • Date: March 9, 2019
  • Place: Indiana University, Bloomington
  • Organizer:  Kim Rodman karodman@iu.edu


All talks will be held in Luddy Hall, Room 1104.
TimeSaturday, March 9
9 a.m. - 9:45 a.mWelcome/coffee
9:45 a.m. - 10:45 a.m.Michael Shulman (University of San Diego)
10:45 a.m. - 11 a.m.Break
11 a.m - 12 p.m.Zachery Lindsey (University of Western Ontario)
12 p.m. - 1:30 p.m.Lunch
1:30 p.m. - 2:30 p.m.Robert Rose (Indiana University)
2:30 p.m. - 2:45 p.m.Break
2:45 p.m. - 3:45 p.m.Noah Snyder (Indiana University)
3:45 p.m. - 4:00 p.m.Break
4 p.m. - 5 p.m.Luis Scoccola (University of Western Ontario)


  • Michael Shulman (University of San Diego), On modeling homotopy type theory in higher toposes

    Abstract: It has been conjectured for many years that homotopy type theory can be interpreted into higher toposes, in a similar way to how higher-order logic can be interpreted into 1-toposes. This would allow the use of type theory as an "internal logic" to prove theorems directly about higher toposes, without the need to manually translate from type-theoretic language into higher-categorical language. The main remaining obstacle to such an interpretation is finding a class of model categories that present all higher toposes and contain strict univalent universes. I will present some recent progress on this problem.

  • Zachery Lindsey (University of Western Ontario)

  • Robert Rose (Indiana University) "Constructing the natural numbers in intensional type theories with S1”

    Abstract: Constructing the natural numbers in intensional type theories with S1 Rijke and Shulman conjectured that the higher inductive type S1 might be viewed as an "axiom of infinity": that well-founded types, such as the natural numbers, with their induction principles, might be obtained from the loop space of S1 in a subtheory of impredicative book HoTT. At last year's seminar, I presented a positive answer to this question; this year I will discuss progress on its formalization and automation. The derived induction principle for the natural numbers applies to families of types in the cumulative hierarchy of univalent universes (with propositional resizing). Of foundational interest, the proof would also go through in settings where suitable large elimination rules and a univalent universe of propositions, but not necessarily univalent universes, are available.

  • Luis Scoccola (University of Western Ontario), “Nilpotent Types and Fracture Squares in Homotopy Type Theory

    Abstract: I will explain how to set up the basic theory of nilpotent spaces and their localizations away from sets of numbers in Homotopy Type Theory. For this, general results about fibrations with fiber an Eilenberg-Mac Lane space are proven, generalizing the classical characterization of nilpotent spaces. I will also give a construction of a fracture square for localizations away from sets of numbers.

  • Noah Snyder (Indiana University), “The encode/decode method for mathematicians

    Abstract: The goal of this talk is to reframe the encode/decode method in a way that a typical working mathematician would understand. The typical problem that encode/decode is trying to solve is to show that a typedescribed by generators and relations has an explicit description where you can detect whether elements are trivial or not. The simplest example of this in mathematics is describing elements of a free group as words on the generators, or more generally solving the word problem for a presentation of a group. This is usually done by giving a free and transitive action of a group on some well-understood set. I will explain how the encode/decode method is a natural generalization of this idea. If time permits I will also discuss using encode/decode to directly understand the 2-trunctations of $\Omega^2S^3$ and $\Omega^3 S^4$. This is related to joint work with my graduate student Nachiket Karnick and my REU student Jacob Prinz.


Please note that there is no registration fee.

Register now


The lot just east of Luddy Hall (on N. Forrest Ave.) is nearest and most convenient.

* Permits are required to park on the IU campus.*


Participants should arrange their own accommodations. We have negotiated a preferred rate of $114 per night at the following hotel for March 8-10:

Graduate Bloomington
210 E Kirkwood Ave
Bloomington, IN 47408
Booking link: IU Informatics and Computer Science Graduate Bloomington March 2019

In the event that all rooms are no longer available under this booking code, please contact Kim Rodman for assistance (karodman@iu.edu)