#Contents# * table of contents {:toc} ## Definition ## A __$\mathcal{U}$-large suplattice__ is a [[lattice]] $(L, \leq, \bot, \vee, \top, \wedge)$ with * a family of functions $$T:\mathcal{U} \vdash \Vee_{n:\mathcal{T}_\mathcal{U}(T)} (-)(n): (\mathcal{T}_\mathcal{U}(T) \to L) \to L$$ * a family of dependent terms $$T:\mathcal{U}, n:\mathcal{T}_\mathcal{U}(T), s:\mathcal{T}_\mathcal{U}(T) \to L \vdash i(n, s):s(n) \leq \Vee_{n:\mathcal{T}_\mathcal{U}(T)} s(n)$$ * a family of dependent terms $$T:\mathcal{U}, x:L, s:\mathcal{T}_\mathcal{U}(T) \to L \vdash i(s, x):\left(\prod_{n:\mathcal{T}_\mathcal{U}(T)}(s(n) \leq x)\right) \to \left(\Vee_{n:\mathcal{T}_\mathcal{U}(T)} s(n) \leq x\right)$$ representing that all $\mathcal{U}$-small joins exist in the lattice. ## See also ## * [[lattice]] * [[frame]]