For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few: UniMath (http

For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few: UniMath (https://github.com/UniMath/UniMath https://github.com/UniMath/UniMath, mentioned in the article) Coq-HoTT (https://github.com/HoTT/Coq-HoTT https://github.com/HoTT/Coq-HoTT) agda-unimath (https://unimath.github.io/agda-unimath/ https://unimath.github.io/agda-unimath/) cubical agda (https://github.com/agda/cubical https://github.com/agda/cubical) All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).