Nuprl Definition : fill_from_comp
fill_from_comp(Gamma;A;comp) ==
λI,i,rho,phi,u,a0. eval j = new-name(I+i) in
comp I+i j m(i;j)(rho) fl-join(I+i;s(phi);(i=0)) fillterm(Gamma;A;I;i;j;rho;a0;u) (a0 (i0)(rho) s)
Definitions occuring in Statement :
fillterm: fillterm(Gamma;A;I;i;j;rho;a0;u),
cubical-type-ap-morph: (u a f),
fl-join: fl-join(I;x;y),
face-presheaf: 𝔽,
fl0: (x=0),
cube-set-restriction: f(s),
nc-m: m(i;j),
nc-0: (i0),
nc-s: s,
new-name: new-name(I),
add-name: I+i,
callbyvalue: callbyvalue,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
callbyvalue: callbyvalue,
new-name: new-name(I),
apply: f a,
nc-m: m(i;j),
fl-join: fl-join(I;x;y),
face-presheaf: 𝔽,
fl0: (x=0),
fillterm: fillterm(Gamma;A;I;i;j;rho;a0;u),
cubical-type-ap-morph: (u a f),
nc-s: s,
cube-set-restriction: f(s),
add-name: I+i,
nc-0: (i0)
FDL editor aliases :
fill_from_comp
Latex:
fill\_from\_comp(Gamma;A;comp) ==
\mlambda{}I,i,rho,phi,u,a0. eval j = new-name(I+i) in
comp I+i j m(i;j)(rho) fl-join(I+i;s(phi);(i=0))
fillterm(Gamma;A;I;i;j;rho;a0;u)
(a0 (i0)(rho) s)
Date html generated:
2016_05_19-AM-09_27_29
Last ObjectModification:
2015_11_09-AM-11_08_11
Theory : cubical!type!theory
Home
Index