Skip to content

HoTT Library

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.

You can’t perform that action at this time.