Vojtěch Štěpančík

How are the changes to descent related to anodyne maps? I can't see from just reading the changes on GitHub where you need those.

> By the way, how do you feel about renaming "descent data of pushouts" to "reduced descent data of pushouts"? I don't see a reason to. The current development uses...

An alternative is to call the type with two equivalences "equifibered spans", precisely because they mirror the shape of a span. For sequential colimits the two notions agree, and the...

I was suggesting that if you have a span `σ : A B`, then you can call the type `(PA : A -> UU) * (PS : S -> UU)...

There's precedent for calling dependent structures "fibered"/"over" and their instantiation at a point `a` "fiber at `a`"/"over `a`" , and not reserving those just for the unstraightened versions; both in...

According to [pre-commit docs](https://pre-commit.com/#command-line-interface), the exit code indicates whether the error was expected (a hook discovered an error) or unexpected (a hook blew up). I'm not sure if that's sufficient...

For context, here's the undetected bad link from the linked PR: `[sublinear rational Cauchy approximations](metric-spaces.sublinear-approximation-ℚ.md)`. Okay, this was pretty tough to track down. When deciding if a link target is...

There is one issue with `--build-library`, and it's that it doesn't open the top-level modules `public`. This already lead to a bug #992, where we had duplicated names between top-level...

That's probably the best we can do, though the `--build-library` flag was introduced to make "standard usage of Everything.agda superfluous", and I don't think opening all modules to prevent duplicate...

> I haven't yet figured out how to prove the extensionality of monoids Hope this helps https://gist.github.com/VojtechStep/d35d246978d627ddd4d2e60514ba7a65