agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
> I tried renaming `elim-ℤ` to `ind-ℤ`, but it turns out that that's already defined in `elementary-number-theory.integers`. The existing one isn't marked abstract, so it computes definitionaly and doesn't need...
Similar to #664. To fix this, `custom.js` should probably use `.gitignore` to filter files.
Following a suggestion made by @jonaprieto () I'll record here an issue about potential ways to make our pre-commit hooks usable by third-parties.
make pre-commit often gives an error on the first run, and then a second run is required which runs then without errors. It looks like this process could be streamlined...
Following Emily Riehl, Jonathan Weinberger, and Nikolai Kudasov's example over at , I think we should port to using ``s ([scalable vector graphics](https://en.wikipedia.org/wiki/SVG)) rather than ASCII diagrams, as these look...
The first middle-dot is · ("MIDDLE DOT", codepoint #xb7), and it's used in left and right whiskering (`_·l_` and `_·r_` in `foundation-core.homotopies`). The other one is ∙ ("BULLET OPERATOR", codepoint...
### The problem On the main page of the docs, when you scroll through all of the modules or follow a reference to a specific place in this index, it...
Defines null-homotopic maps and characterizes their equality. In particular, a sufficient condition for when being null-homotopic is a property is given.