Vojtěch Štěpančík
Vojtěch Štěpančík
I prefer not quoting the arguments for `general-def`, including in the `:general` section of a use-package clause. This usually results in expressions like the following: ```elisp :general ((motion normal) global...
Right now, AFAICT, the domain resolution for different `:host`s has a hardcoded dictionary of mappings from a host to a domain. I would like to be able to change this...
On my machine, the folder `/usr/java` does not exist, and apparently that crashes the server (logs below). I can see that in the `JavaHomeHelper` class, some folders are tested for...
In anticipation for #885. The proof of the universal property of coequalizers being preserved by equivalences of coforks got a bit unwieldy, but it should become more conceptual once morphisms...
In https://github.com/UniMath/agda-unimath/pull/1056#discussion_r1519953433 @EgbertRijke raised the question whether we should keep with the type theory convention of having "isomorphisms" be in general maps with structure, or if we should reappropriate it...
This PR formalizes shifts of sequential diagrams, morphisms of sequential diagrams, cocones of sequential diagrams, homotopies of cocones of sequential diagrams, and unshifts of the last two. This machinery is...
I already formalized and documented parts of the paper. I'm assigning myself, because I would like to include this formalization effort in my master's thesis.
We have a GitHub action for typechecking the library with performance tracking on master, but it would be nice to know what impact a PR has before merging it, so...
That's an almost 3MB over the wire (17MB on disk) file that should only be downloaded when the users opens the search bar for the first time
> 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...