https://unimath.github.io/agda-unimath/order-theory.least-upper-bounds-large-posets.html
Least upper bounds in large posets - agda-unimath
A community-driven library of formalized mathematics from a univalent point of view using the dependently typed programming language Agda.
least upper boundslargeposetsagda