Nuprl Definition : pi-comp-app
pi-comp-app(Gamma;A;I;i;rho;phi;mu;J;f;j;nu) ==
app((mu)subset-trans(I+i;J+j;f,i=j;s(phi)); (canonical-section(Gamma;A;J+j;f,i=j(rho);nu))iota)
Definitions occuring in Statement :
cubical-app: app(w; u),
csm-ap-term: (t)s,
canonical-section: canonical-section(Gamma;A;I;rho;a),
subset-trans: subset-trans(I;J;f;x),
subset-iota: iota,
face-presheaf: 𝔽,
cube-set-restriction: f(s),
nc-e': g,i=j,
nc-s: s,
add-name: I+i
Definitions occuring in definition :
cubical-app: app(w; u),
subset-trans: subset-trans(I;J;f;x),
face-presheaf: 𝔽,
nc-s: s,
csm-ap-term: (t)s,
subset-iota: iota,
canonical-section: canonical-section(Gamma;A;I;rho;a),
cube-set-restriction: f(s),
add-name: I+i,
nc-e': g,i=j
FDL editor aliases :
pi-comp-app
Latex:
pi-comp-app(Gamma;A;I;i;rho;phi;mu;J;f;j;nu) ==
app((mu)subset-trans(I+i;J+j;f,i=j;s(phi)); (canonical-section(Gamma;A;J+j;f,i=j(rho);nu))iota)
Date html generated:
2016_05_19-AM-09_37_55
Last ObjectModification:
2016_01_25-PM-04_29_26
Theory : cubical!type!theory
Home
Index