Nuprl Definition : pi-comp
pi-comp(Gamma;A;B;cA;cB) ==
λI,i,rho,phi,mu,lambda,J,f,u1. eval j = new-name(J) in
let nu = pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u1;j) in
cB J j (f,i=j(rho);nu) f(phi) pi-comp-app(Gamma;A;I;i;rho;phi;mu;J;f;j;nu)
pi-comp-lambda(Gamma;A;I;i;rho;lambda;J;f;j;nu)
Definitions occuring in Statement :
pi-comp-lambda: pi-comp-lambda(Gamma;A;I;i;rho;lambda;J;f;j;nu),
pi-comp-app: pi-comp-app(Gamma;A;I;i;rho;phi;mu;J;f;j;nu),
pi-comp-nu: pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u1;j),
cc-adjoin-cube: (v;u),
face-presheaf: 𝔽,
cube-set-restriction: f(s),
nc-e': g,i=j,
new-name: new-name(I),
add-name: I+i,
callbyvalue: callbyvalue,
let: let,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
callbyvalue: callbyvalue,
new-name: new-name(I),
let: let,
pi-comp-nu: pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u1;j),
apply: f a,
cc-adjoin-cube: (v;u),
add-name: I+i,
nc-e': g,i=j,
cube-set-restriction: f(s),
face-presheaf: 𝔽,
pi-comp-app: pi-comp-app(Gamma;A;I;i;rho;phi;mu;J;f;j;nu),
pi-comp-lambda: pi-comp-lambda(Gamma;A;I;i;rho;lambda;J;f;j;nu)
FDL editor aliases :
pi-comp
Latex:
pi-comp(Gamma;A;B;cA;cB) ==
\mlambda{}I,i,rho,phi,mu,lambda,J,f,u1. eval j = new-name(J) in
let nu = pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u1;j) in
cB J j (f,i=j(rho);nu) f(phi)
pi-comp-app(Gamma;A;I;i;rho;phi;mu;J;f;j;nu)
pi-comp-lambda(Gamma;A;I;i;rho;lambda;J;f;j;nu)
Date html generated:
2016_05_19-AM-09_40_02
Last ObjectModification:
2016_01_25-PM-10_43_01
Theory : cubical!type!theory
Home
Index