#Contents# * table of contents {:toc} ## 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 $$T:\mathcal{U}, a:L, s:\mathcal{T}_\mathcal{U}(T) \to L \vdash a \wedge \Vee_{n:\mathcal{T}_\mathcal{U}(T)} s(n) = \Vee_{n:\mathcal{T}_\mathcal{U}(T)} a \wedge s(n)$$ 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, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)