Title: Impredicative encodings in homotopy type theory
Speaker: Steve Awodey (Carnegie-Mellon)
Abstract: We present some recent results on impredicative encodings of inductive types (including higher inductive types) in HoTT. It is well-known that encoding inductives using higher-order quantification (i.e. quantification over all types) provides a potential theoretical and practical simplification of the type system.
Using the further resources available in HoTT permits a sharpening of the usual System F style, impredicative encodings, but this begs the question of whether impredicativity is compatible with univalence. We give a realizability model using a combination of topos-theoretic, homotopical, and recent cubical methods. (Joint work with Jonas Frey and Pieter Hofstra.)
