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