The Groupoid Infinity Cubical Base Library is dedicated to cubical-compatible
typecheckers based on homotopy interval [0,1] and MLTT as a core.
The library follows HoTT foundation and mathematics partitioning: the
chapter covers the very basics of the cubical programming language; the
chapter covers the formal mathematics library of models and theorems.
This library is best to read with HoTT book at http://groupoid.space/math/
- Namdak Tonpa
- Siegmentation Fault
- Eugene Smolanka
- Andy Melnikov
- Denis Stoyanov
- Dmitry Astapov