Jacques Carette

As stand-alone code, this is great. But this also represents a non-trivial new design, and there's various things I am not so sure about. I don't want to merge this...

I agree that splitting off the immediately mergable stuff into a separate PR is a good idea. As to the rest, you'll need to explicitly prod some not-me reviewers into...

My understanding is that the reason for all this back-and-forth is that the hierarchy was too coarse initially, and so things that ought to have been true weren't because there...

I agree. The beauty of dependently-typed programming is that we can now express this "emergent knowledge" in the types, so that it doesn't have to be rediscovered by later code....

I picture `Pointed` as a *theory*, so a record. What `Relation.Nullary.Construct.Add.Point` does is build the **free** `Pointed` on a `Set`, as @jamesmckinna says. `Maybe` isn't a theory, it's a data-structure...

I still see it as something that belongs in `Algebra`. It could be called `Pointed` but also `PointedCarrier`, `PointedSet`, `PointedSetoid`, I'm ok with all of those.

I've found `toFunction` and `fromFunction` for `Inverse` in `Function.Properties.Inverse`. But I agree that this is inconsistent with what is done in `Equivalence` which defines them locally.

I agree that this would be pronounced "factors divide" and so a name that puts things in the same order makes sense.

@Taneb that was my instinct as well, but then all the `cast` needed a `sym` which was a clear sign to me that things were the wrong way around! There's...

Yes, I still would like to keep this open. I will want to come back to it, when I have a bit of time to breathe. Stupid admin job.