skip to content

Impredicative encodings in HoTT

Presented by: 
Steve Awodey
Tuesday 11th July 2017 - 09:00 to 10:00
INI Seminar Room 1
We investigate the prospects for impredicative encodings of inductive types (including higher inductive types) in HoTT.  It is well-known that encoding inductives using higher-order quantification provides a potential theoretical and practical simplification of the system.  Using the further resources available in HoTT allows for a sharpening of the familiar System F style impredicative encodings of inductive types, but this begs the question of whether impredicativity is formally 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.
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons