Presented by:
Steve Awodey
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.
The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.