Impredicative encodings in HoTT
54 mins 35 secs,
99.84 MB,
MP3
44100 Hz,
249.74 kbits/sec
Share this media item:
Embed this media item:
Embed this media item:
About this item
Description: |
Awodey, S
Tuesday 11th July 2017 - 09:00 to 10:00 |
---|
Created: | 2017-07-26 12:40 |
---|---|
Collection: | Big proof |
Publisher: | Isaac Newton Institute |
Copyright: | Awodey, S |
Language: | eng (English) |
Distribution: | World (downloadable) |
Explicit content: | No |
Aspect Ratio: | 16:9 |
Screencast: | No |
Bumper: | UCS Default |
Trailer: | UCS Default |
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. |
---|
Available Formats
Format | Quality | Bitrate | Size | |||
---|---|---|---|---|---|---|
MPEG-4 Video | 640x360 | 1.93 Mbits/sec | 793.11 MB | View | Download | |
WebM | 640x360 | 579.01 kbits/sec | 231.27 MB | View | Download | |
iPod Video | 480x270 | 521.62 kbits/sec | 208.34 MB | View | Download | |
MP3 * | 44100 Hz | 249.74 kbits/sec | 99.84 MB | Listen | Download | |
Auto | (Allows browser to choose a format it supports) |