skip to content

The Lean HoTT library

Presented by: 
Floris van Doorn
Friday 7th July 2017 - 11:30 to 12:00
INI Seminar Room 2
An overview of the homotopy type theory library in Lean, in comparison towards the other proof assistants available for HoTT. This talk is more aimed towards the HoTT community. A second talk will be given during the workshop which is more aimed towards the formal verification community.
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.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons