skip to content
 

Impredicative encodings in HoTT

Presented by: 
Steve Awodey Carnegie Mellon University
Date: 
Tuesday 11th July 2017 - 09:00 to 10:00
Venue: 
INI Seminar Room 1
Abstract: 

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.

Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons