Towards elementary infinity-toposes

Abstract: Toposes were invented by Grothendieck to abstract properties of categories of sheaves, but soon Lawvere and Tierney realized that the elementary (i.e. "finitary" or first-order) properties satisfied by Grothendieck's toposes were precisely those characterizing a "generalized category of sets". An elementary topos shares most of the properties of Grothendieck's, as well as supporting an "internal language" that enables it to be used as a basis for mathematics. Now, recently Toen-Vezzosi, Rezk, Lurie, and others have generalized Grothendieck's toposes of sheaves to infinity-toposes of stacks, while Awodey-Warren, Voevodsky, and others have invented Homotopy Type Theory and Univalent Foundations as an "infinity-logic" that is expected to act as an internal language for infinity-toposes. However, an "elementary" notion of infinity-topos analogous to Lawvere and Tierney's elementary toposes has been lacking. I will give an introduction to this problem and survey recent progress on it.