Vojtěch Štěpančík
Vojtěch Štěpančík
From #1472: > I'm still working on the extensionality of Monoid with respect to isomorphisms, not just equivalences I updated the gist, it now includes a proof that isomorphisms of...
What's the criteria for closing this issue? Replacing our dependency on nixpkgs with a dependency on the agda repo? I'd rather not do this, as that one doesn't have a...
I'm pretty sure this broke the `interactive` highlight level for me, the highlighting does not go away. I'll keep testing and digging further
> I haven't yet figured out if you can do it with just truncation the way agda-unimath seems to. I'm not an expert, but while I'd expect just truncations to...
Actually I'm not really sure what's happening — the suggested heap size is at 4GB for the CI, and the benchmarks do show pretty consistent memory usage at around 4GB...
> bug on the mdbook or katex side Neither one tries to interpret this as a link, if anything it's an issue with linkcheck. Good news is that there is...
@EgbertRijke do you have a timeline in mind for finishing this PR? I'm not sure if I should be continuing my development with the old infrastructure, or if it's feasible...
Great! Thanks
Do you have a reference for this concept 👀? I'd like to see what the "variables" refer to, and why I should think about non-generalized loop spaces as "bivariable"
Note that we don't have a concept of stable identifiers. We try to approximate a reasonably stable one by trying, in order of most priority to least: - the linked...