Port pointwise adjunctions from catdb

It is, unfortunately, the slowest thing in the repo to date, by a factor
of two.  (It's much faster in the pinned version of Coq, though, than in current trunk.)