Homotopy Type Theory frame > history (Rev #2)

Contents

Definition

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

References

Revision on April 25, 2022 at 10:40:56 by Anonymous?. See the history of this page for a list of all contributions to it.