Nuprl Definition : pi-comp-nu
pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u1;j) ==
let v' = fill_from_comp(Gamma;A;cA) J j f,i=1-j(rho) 0 () u1 in
(v' f,i=1-j(rho) r_j)
Definitions occuring in Statement :
fill_from_comp: fill_from_comp(Gamma;A;comp),
trivial-section: (),
cubical-type-ap-morph: (u a f),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
nc-r': g,i=1-j,
nc-r: r_i,
add-name: I+i,
lattice-0: 0,
let: let,
apply: f a
Definitions occuring in definition :
let: let,
apply: f a,
fill_from_comp: fill_from_comp(Gamma;A;comp),
lattice-0: 0,
face_lattice: face_lattice(I),
trivial-section: (),
cubical-type-ap-morph: (u a f),
nc-r: r_i,
cube-set-restriction: f(s),
add-name: I+i,
nc-r': g,i=1-j
FDL editor aliases :
pi-comp-nu
Latex:
pi-comp-nu(Gamma;A;cA;I;i;rho;J;f;u1;j) ==
let v' = fill\_from\_comp(Gamma;A;cA) J j f,i=1-j(rho) 0 () u1 in
(v' f,i=1-j(rho) r\_j)
Date html generated:
2016_05_19-AM-09_36_18
Last ObjectModification:
2016_01_25-PM-04_19_03
Theory : cubical!type!theory
Home
Index