Homotopy Type Theory suplattice > history (Rev #1)

Contents

Definition

A 𝒰\mathcal{U}-large suplattice is a lattice (L,,,,,)(L, \leq, \bot, \vee, \top, \wedge) with

  • a family of functions

    T:𝒰 n:𝒯 𝒰(T)()(n):(𝒯 𝒰(T)L)LT:\mathcal{U} \vdash \Vee_{n:\mathcal{T}_\mathcal{U}(T)} (-)(n): (\mathcal{T}_\mathcal{U}(T) \to L) \to L
  • a family of dependent terms

    T:𝒰,n:𝒯 𝒰(T),s:𝒯 𝒰(T)Li(n,s):s(n) n:𝒯 𝒰(T)s(n)T:\mathcal{U}, n:\mathcal{T}_\mathcal{U}(T), s:\mathcal{T}_\mathcal{U}(T) \to L \vdash i(n, s):s(n) \leq \Vee_{n:\mathcal{T}_\mathcal{U}(T)} s(n)
  • a family of dependent terms

    T:𝒰,x:L,s:𝒯 𝒰(T)Li(s,x):( n:𝒯 𝒰(T)(s(n)x))( n:𝒯 𝒰(T)s(n)x)T:\mathcal{U}, x:L, s:\mathcal{T}_\mathcal{U}(T) \to L \vdash i(s, x):\left(\prod_{n:\mathcal{T}_\mathcal{U}(T)}(s(n) \leq x)\right) \to \left(\Vee_{n:\mathcal{T}_\mathcal{U}(T)} s(n) \leq x\right)

representing that all 𝒰\mathcal{U}-small joins exist in the lattice.

See also

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