working on Poly.

- All of the admitted definitions are about dependent
  contexts.
- There should be a similar interface that abstracts
  the relevant bits for this but it isn't the same simple
  structures because they use [Pi] instead of [->]