Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
In the section As a category, I have hyperlinked a couple of “Equivalently we may…” and “In other words we…” to the new entry relation between preorders and (0,1)-categories.
Fixed section on HoTT preorders/partial orders. The terminology in use before was incoherent and fairly inconsistent (e.g. using ∧ to stand for transitivity) and while preorders and equivalence relations are both symmetric and transitive, it detracts from the exposition on this page to smush them together. Preorders are more naturally generalised to partial orders.
Added a paragraph explaining that partial orders in HoTT force the type they apply to be an h-set.
moving Theorem 3.1 and its proof from specialization order to preorder because the proof applies to all binary relations, not just that of the membership relation between elements and open sets of a topological space.
1 to 4 of 4