Nuprl Definition : face-forall
(∀ phi) == λJ,rho. (∀new-name(J).phi((s(rho);<new-name(J)>)))
Definitions occuring in Statement :
cc-adjoin-cube: (v;u),
cubical-term-at: u(a),
fl_all: (∀i.phi),
cube-set-restriction: f(s),
nc-s: s,
new-name: new-name(I),
add-name: I+i,
dM_inc: <x>,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
fl_all: (∀i.phi),
cubical-term-at: u(a),
cc-adjoin-cube: (v;u),
cube-set-restriction: f(s),
add-name: I+i,
nc-s: s,
dM_inc: <x>,
new-name: new-name(I)
FDL editor aliases :
face-forall
Latex:
(\mforall{} phi) == \mlambda{}J,rho. (\mforall{}new-name(J).phi((s(rho);<new-name(J)>)))
Date html generated:
2016_05_19-AM-08_30_12
Last ObjectModification:
2016_03_25-PM-02_18_24
Theory : cubical!type!theory
Home
Index