Skip to content
This repository was archived by the owner on Oct 14, 2023. It is now read-only.

HoTT Library

Jump to bottom
Floris van Doorn edited this page Oct 18, 2017 · 8 revisions

  • The biggest HoTT library is in Lean2, together with a formalization of the Serre Spectral Sequence in a separate repository.

  • We are also working on an version in Lean 3 here without any kernel modification. Porting the library from Lean 2 is in progress.

Clone this wiki locally