Formalize the notion of density in a strict poset

[lowasser]

This will necessarily have to be different for large strict posets, too, which I'm not even sure exist yet?

[fredrik-bakke]

Indeed, large strict posets are not formalized in the library as of yet.

By the way, do you know what the appropriate extensionality principle for a strict poset is? We have the notion of a strictly preordered set, but this structure is not extensional. For posets, extensionality is antisymmetry, but every strict order is trivially antisymmetric. The main idea that comes to mind is to extend the extensionality principle of ordinals:

$$((u : X) → (u < x) ↔ (u < y)) → x ＝ y$$

but taking both directions into account, i.e.,

$$((u : X) → (u < x) ↔ (u < y)) → ((v : X) → (x < v) ↔ (y < v)) → x ＝ y$$

[fredrik-bakke]

Actually, thinking a little more about this, this principle has to be the correct one for strict posets. In The Univalence Principle, Example 8.16 they consider the extensionality principle for semicategories (these are not-necessarily-unital categories), which subsume strict orders. The extensionality principle for semicategories specializes precisely to the condition I wrote out above, so it should be the correct condition.

[fredrik-bakke]

This will necessarily have to be different for large strict posets, too, which I'm not even sure exist yet?

Here you go: #1419