Groupoid Infinity Institute is doing formalization of mathematics in the formal programming language called Anders 1.3.0 , a CCHM/HTS variant of cubical type systems .
Mathematical theories, models and languages.
Homotopy Library for Anders theorem prover consists of two parts Foundations and Mathematics just as HoTT Book .