Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

< frame

category: redirected to nlab

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.

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

Last revised on June 10, 2022 at 15:43:14. See the history of this page for a list of all contributions to it.