UniMath Alternatives
Similar projects and alternatives to UniMath


SaaSHub
SaaSHub  Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives






TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.

coqlibraryundecidability
A library of mechanised undecidability proofs in the Coq proof assistant.




UniMath discussion
UniMath reviews and mentions

Will Computers Redefine the Roots of Math?
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, mentioned in the article)
CoqHoTT (https://github.com/HoTT/CoqHoTT)
agdaunimath (https://unimath.github.io/agdaunimath/)
cubical agda (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).

Are There People Doing Formal Math In Berlin?
I just wonder if there are any irl meetups of people involved with formalizing mathematics, I thought that it would be a cool hobby to pick up (with some background in math and programming) but the existing libraries, like MathLib, TypeTopology or UniMath look a bit intimidating...
Stats
UniMath/UniMath is an open source project licensed under GNU General Public License v3.0 or later which is an OSI approved license.
The primary programming language of UniMath is Coq.