What does HackerNews think of UniMath?

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

Language: Coq

Will Computers Redefine the Roots of Math? | Jun 2023
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)

Coq-HoTT (https://github.com/HoTT/Coq-HoTT)

agda-unimath (https://unimath.github.io/agda-unimath/)

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).

Number Theorist Fears All Published Math Is Wrong | Sep 2019
Sounds like a sales pitch for Lean (Microsoft's theorem prover), even though Coq [1] is the standard tool for the UniMath [2] project.

[1] https://en.wikipedia.org/wiki/Coq

[2] https://github.com/UniMath/UniMath

P=NP Proofs – Advice to claimers | Apr 2019
Expand Context ↕
There’s other efforts, like the UniMath project by the HoTT people.

https://github.com/UniMath/UniMath
Making math more Lego-like | Mar 2017
Expand Context ↕
> abstract, human-evaluatable, programming language?

yes, it's happening: https://ncatlab.org/nlab/show/Globular

> Use logically derived variable names

I agree. It just becomes a pain in the ass to write this stuff. The greek is math-asm for the hand.

> completely standard way as to how to define all of your algorithms and logical assertions?

people are working on it, for example: https://github.com/UniMath/UniMath "This coq library aims to formalize a substantial body of mathematics using the univalent point of view."

One thing to note however is that the mathematics in the OP is inherently two (and higher) dimensional, and so it makes much more sense to adopt a language that is two (or higher) dimensional. Squashing it down into one dimensions (like with a usual language) creates a big mess.
Will Computers Redefine the Roots of Math? | May 2015
See https://github.com/UniMath/UniMath for more!