The HoTT library in Coq
1 hour 32 mins,
330.47 MB,
iPod Video
480x270,
29.97 fps,
44100 Hz,
490.43 kbits/sec
Share this media item:
Embed this media item:
Embed this media item:
About this item
| Description: |
Spitters, B
Friday 7th July 2017 - 11:00 to 11:30 |
|---|
| Created: | 2017-07-24 17:40 |
|---|---|
| Collection: | Big proof |
| Publisher: | Isaac Newton Institute |
| Copyright: | Spitters, B |
| Language: | eng (English) |
| Distribution: |
World
(downloadable)
|
| Explicit content: | No |
| Aspect Ratio: | 16:9 |
| Screencast: | No |
| Bumper: | UCS Default |
| Trailer: | UCS Default |
| Abstract: | We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters, The HoTT Library: A formalization of homotopy type theory in Coq (CPP17) pp. 164-172, 2017 10.1145/3018610.3018615 https://arxiv.org/abs/1610.04591 |
|---|---|
Available Formats
| Format | Quality | Bitrate | Size | |||
|---|---|---|---|---|---|---|
| MPEG-4 Video | 640x360 | 1.91 Mbits/sec | 1.29 GB | View | Download | |
| WebM | 640x360 | 453.36 kbits/sec | 305.49 MB | View | Download | |
| iPod Video * | 480x270 | 490.43 kbits/sec | 330.47 MB | View | Download | |
| MP3 | 44100 Hz | 250.86 kbits/sec | 169.04 MB | Listen | Download | |
| Auto | (Allows browser to choose a format it supports) | |||||