Homotopy Type Theory frame > history (Rev #1)

Contents

Definition
See also
References

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.

See also

References

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

Revision on April 22, 2022 at 01:03:34 by Anonymous?. See the history of this page for a list of all contributions to it.