Logic in univalent type theory

57 mins 20 secs,  104.89 MB,  MP3  44100 Hz,  249.77 kbits/sec
Share this media item:
Embed this media item:


About this item
Image inherited from collection
Description: Escardo, M
Tuesday 11th July 2017 - 10:00 to 11:00
 
Created: 2017-07-26 12:45
Collection: Big proof
Publisher: Isaac Newton Institute
Copyright: Escardo, M
Language: eng (English)
Distribution: World     (downloadable)
Explicit content: No
Aspect Ratio: 16:9
Screencast: No
Bumper: UCS Default
Trailer: UCS Default
 
Abstract: We explain and illustrate the logic used in univalent type theory, and we compare it to the usual Curry-Howard logic used in Martin-Loef type theory.
Available Formats
Format Quality Bitrate Size
MPEG-4 Video 640x360    1.93 Mbits/sec 830.42 MB View Download
WebM 640x360    655.27 kbits/sec 274.92 MB View Download
iPod Video 480x270    520.52 kbits/sec 218.39 MB View Download
MP3 * 44100 Hz 249.77 kbits/sec 104.89 MB Listen Download
Auto (Allows browser to choose a format it supports)