LIBRARY

HOMOTOPY LIBRARY

Homotopy Library for Anders proof assistant consists of two parts Foundations and Mathematics just as HoTT Book.

Foundations

MLTT, Modal and Univalent Foundations represent a basic language primitives of Anders and its base library.

Mathematics

The second part is dedicated to mathematical models and theories internalized in this language.


The base library for cubicaltt is given on separate page: Formal Mathematics: The Cubical Base Library