Impredicative encodings in HoTT

Add to your list(s) Download to your calendar using vCal

• Steve Awodey (Carnegie Mellon University)
• Tuesday 11 July 2017, 09:00-10:00
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact INI IT.

BPRW01 - Computer-aided mathematical proof

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.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.