Apostolisapostolis@social.coop
Feb 14, 2025, 9:04 AM@khinsen Apart from not being a logician, the error messages do not explain the algorithms.
Also, Agda is a research project, meaning that new theories are always introduced. This is good and bad. A lot of errors can be found later.
This has led many to limit themselves to a well understood part of theory, check for example @MartinEscardo typetopology .
In the same vein, I use univalent mathematics, math in general, well understood concepts, instead of Agda 's features.
