Homotopy Type Theory frame > history (changes)

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


< frame


A 𝒰\mathcal{U}-large frame is a 𝒰\mathcal{U}-large suplattice (L,,,,,,)(L, \leq, \bot, \vee, \top, \wedge, \Vee) with a family of dependent terms

T:𝒰,a:L,s:𝒯 𝒰(T)La n:𝒯 𝒰(T)s(n)= n:𝒯 𝒰(T)as(n)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


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