Post #1816219
2026-02-24 06:18 UTC
@OscarCunningham I don't know about the MO question, but suplattices have a prop-valued reflexive and antisymmetric relation and any type with such a relation is necessarily a set. This can be seen with a much simpler argument using what @MartinEscardo calls local Hedberg. https://martinescardo.github.io/TypeTopology/UF.HedbergApplications.html#2299
@dwarn
Replies (1)
-
@OscarCunningham@mathstodon.xyz 2026-02-24 06:55
@de_Jong_Tom @dwarn Cool. In particular, people sometimes define lattices in terms of their partial order, and sometimes in terms of their algebraic operations. So it's useful to know that we can prove they're discrete either way.