Nuprl Definition : pi-comp-lambda
pi-comp-lambda(Gamma;A;I;i;rho;lambda;J;f;j;nu) == lambda J f (nu r_j(f,i=1-j(rho)) (j0))
Definitions occuring in Statement :
cubical-type-ap-morph: (u a f),
cube-set-restriction: f(s),
nc-r': g,i=1-j,
nc-0: (i0),
nc-r: r_i,
add-name: I+i,
apply: f a
Definitions occuring in definition :
apply: f a,
cubical-type-ap-morph: (u a f),
nc-0: (i0),
nc-r: r_i,
cube-set-restriction: f(s),
add-name: I+i,
nc-r': g,i=1-j
FDL editor aliases :
pi-comp-lambda
Latex:
pi-comp-lambda(Gamma;A;I;i;rho;lambda;J;f;j;nu) == lambda J f (nu r\_j(f,i=1-j(rho)) (j0))
Date html generated:
2016_05_19-AM-09_38_25
Last ObjectModification:
2016_01_25-PM-04_52_58
Theory : cubical!type!theory
Home
Index