James Wood

This sounds a bit like a problem I've been having for a long time (maybe a year or so) with Zoom, which I've tended to think has something to do...

If, instead of `Derive NoConfusion for Node.`, I do `Derive Signature NoConfusionHom for Node.`, I get a different error at the last definition: ``` Anomaly "Uncaught exception Failure("Could not generate...

> This raises an important question that I am not qualified to answer. Is the setoid-based definition of `Surjective` named accurately, or not? I think not. In standard mathematical notation...

Here are [Andrej's definitions of *surjective* and *epi* on setoids](https://gist.github.com/andrejbauer/65ee1ae98167e6411e512d3e5a36c086#file-epimorphism-agda), which agree with what I said.

In the non-setoid (`_≡_`) case, it's not clear to me that it makes sense to distinguish between *surjective* and *split-surjective*. We can't even state the distinction in MLTT. In the...

`g` is a setoid morphism (probably it's unclear that the arrow is slightly longer!), so while you can reconstruct its action, that action doesn't necessarily preserve equivalence.

[non-dependent products](https://agda.github.io/agda-stdlib/Data.Product.Relation.Binary.Pointwise.NonDependent.html#7563), [sums](https://agda.github.io/agda-stdlib/Data.Sum.Relation.Binary.Pointwise.html#6974) But yeah, this is a classic problem of having two hierarchies (type formers and order structures), but only reflecting one of them in the module hierarchy.

Is the style guide also the right place for explaining `Core` vs `Base` vs `Properties` vs plain; `Structures`, `Bundles`, &c; and other file placement conventions?

Another funny thing is that `RawMonad` is not a subclass of `RawApplicative`, so the `_⊛_` coming from `monad` is different to the one coming from `applicative`. When I tried just...

#952