Floris van Doorn
Floris van Doorn
> how about adding your picture to your github profile? ok > Kernels of monoid maps are not important, because you can't recover a quotient monoid Y of a monoid...
UniMath/CategoryTheory/categories/abgrs.v line 650-ish. I'm moving what I needed in #831.
Hmm... There are a couple things going on here. I'm also replying to #2005 * First of all, this is very un-idiomatic Lean. Much better would be to do ```lean...
I can reproduce this in `cmd`. As a workaround, the command does work in the `MSYS2 MinGW 64-bit` shell, which you can install [here](https://www.msys2.org/).
@favonia asked me to comment. In Lean we use the definition of `Ωⁿ(X)` where `Ωⁿ⁺¹(X) :≡ Ω(Ωⁿ(X))`. I think that definition is more convenient, even though you wish you sometimes...
I can consistently reproduce this on my Windows machine, but I didn't manage to reproduce it yesterday on my Linux machine (both in VSCode). Here is some behavior that might...
I don't know how often these concepts are used. Feel free to leave it like this if you think it's rarely used.
This comment is also related to #1211. My experience with equivalences in Lean is that type-class inference is too slow and (at least in the case of Lean) too brittle....
> > the lemma stating that if `e : A B` and `e == f` then `IsEquiv f` > > FWIW, I defined that lemma in #1207 as `isequiv_homotopic'`. Ah...