Definition

A $\mathcal{U}$-large frame is a $\mathcal{U}$-large suplattice $(L, \leq, \bot, \vee, \top, \wedge, \Vee)$ with a family of dependent terms

representing that meets distribute over all $\mathcal{U}$-small joins in the lattice.

See also

• suplattice

• distributive lattice

• Dedekind cut (disambiguation)

• Dedekind real numbers (disambiguation)

• geometric dagger 2-poset

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)