Nuprl Definition : context-subset
Gamma, phi == <λI.{rho:Gamma(I)| phi(rho) = 1 ∈ Point(face_lattice(I))} , λI,J,f,rho. f(rho)>
Definitions occuring in Statement :
cubical-term-at: u(a),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
I_cube: A(I),
lattice-1: 1,
lattice-point: Point(l),
set: {x:A| B[x]} ,
lambda: λx.A[x],
pair: <a, b>,
equal: s = t ∈ T
Definitions occuring in definition :
pair: <a, b>,
set: {x:A| B[x]} ,
I_cube: A(I),
equal: s = t ∈ T,
lattice-point: Point(l),
cubical-term-at: u(a),
lattice-1: 1,
face_lattice: face_lattice(I),
lambda: λx.A[x],
cube-set-restriction: f(s)
FDL editor aliases :
context-subset
Latex:
Gamma, phi == <\mlambda{}I.\{rho:Gamma(I)| phi(rho) = 1\} , \mlambda{}I,J,f,rho. f(rho)>
Date html generated:
2016_05_19-AM-08_26_56
Last ObjectModification:
2016_02_23-AM-00_17_51
Theory : cubical!type!theory
Home
Index