Poset Refactor

[TOTBWF]

Description

This PR bundles Poset and monotone maps. This is the first stage of the poset refactor: none of the changes around frames/lattices were made yet!.

Todo:
[ ] Update Prose

[github-actions]

Rendered preview

[favonia]

Question: why do we want opaque when, as far as I can tell, no one will want to unfold Ob-is-set?

[plt-amy]

Good point, from a "say what you mean" perspective those could be abstract; all that it matters is that it doesn't accidentally reduce in someone's face, since it's a pretty nasty term.

[favonia]

@plt-amy Yes I do mean using abstract, the "absolute" opaque. In fact I want to add abstract (and maybe irrelevance) to many definitions in 1lab...