Nuprl Definition : glue-term
glue [phi ⊢→ t] a == λI,rho. if (phi(rho)==1) then t(rho) else <λJ,f. t(f(rho)), a(rho)> fi
Definitions occuring in Statement :
cubical-term-at: u(a),
fl-eq: (x==y),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
lattice-1: 1,
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
fl-eq: (x==y),
lattice-1: 1,
face_lattice: face_lattice(I),
pair: <a, b>,
lambda: λx.A[x],
cube-set-restriction: f(s),
cubical-term-at: u(a)
FDL editor aliases :
glue-term
Latex:
glue [phi \mvdash{}\mrightarrow{} t] a == \mlambda{}I,rho. if (phi(rho)==1) then t(rho) else <\mlambda{}J,f. t(f(rho)), a(rho)> fi
Date html generated:
2016_05_20-AM-08_46_23
Last ObjectModification:
2016_03_03-AM-00_00_14
Theory : cubical!type!theory
Home
Index