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

• 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.

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.*