# Homotopy Type Theory frame > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

# Contents

## 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.