Nuprl Definition : face_comp
face_comp() == λI,i,rho,phi,u,a0. (i1)(extend-face-term(I+i;s(phi);u))
Definitions occuring in Statement :
extend-face-term: extend-face-term(I;phi;u),
face-presheaf: 𝔽,
cube-set-restriction: f(s),
nc-1: (i1),
nc-s: s,
add-name: I+i,
lambda: λx.A[x]
Definitions occuring in definition :
nc-s: s,
add-name: I+i,
face-presheaf: 𝔽,
cube-set-restriction: f(s),
extend-face-term: extend-face-term(I;phi;u),
nc-1: (i1),
lambda: λx.A[x]
FDL editor aliases :
face_comp
Latex:
face\_comp() == \mlambda{}I,i,rho,phi,u,a0. (i1)(extend-face-term(I+i;s(phi);u))
Date html generated:
2017_02_21-AM-11_02_44
Last ObjectModification:
2017_02_07-PM-05_56_54
Theory : cubical!type!theory
Home
Index