agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
Inline latex in a concept name seems to break the macro. E.g., here: https://unimath.github.io/agda-unimath/foundation.hilberts-epsilon-operators.html The raw markdown code: ```md {{#concept "Hilbert's $ε$-operator"}} at a type `A` is a map ```...
In addition to the standard analytic power series in #1354 , we should consider building out the theory of formal power series and polynomials. It's not obvious to me how...
Addition of Cauchy sequences in the reals is cool and all, but we can be more general. There's nothing special about _addition_ as an operation that takes two Cauchy sequences...
I imagine we'd want an entire new folder for complex numbers. This isn't near my top priorities, but it's certainly an area we can build out, and we don't need...
I'm doing some travel with only a Chromebook that can run VSCode and at least edit Agda with all the symbols etc, but doesn't have the capacity (RAM?) to compile...
- Define noncoherent $\omega$-semiprecategories - The universal property of isomorphisms in $\omega$-semicategories - Idempotent and neutral points of a $\omega$-semicategory
As requested in #1306 , starting a new PR for working through the docs.
I was mentioning to someone or another the difficulty of taking reciprocals of natural numbers, or doing anything significant with them, and part of the problem is that things may...