Nuprl Definition : fillterm
fillterm(Gamma;A;I;i;j;rho;a0;u) == λK,f. if isdM0(f i) then (a0 (i0)(rho) s ⋅ f) else u(m(i;j) ⋅ f) fi
Definitions occuring in Statement :
cubical-term-at: u(a),
cubical-type-ap-morph: (u a f),
cube-set-restriction: f(s),
nc-m: m(i;j),
nc-0: (i0),
nc-s: s,
add-name: I+i,
nh-comp: g ⋅ f,
isdM0: isdM0(x),
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
isdM0: isdM0(x),
apply: f a,
cubical-type-ap-morph: (u a f),
nc-s: s,
cube-set-restriction: f(s),
nc-0: (i0),
cubical-term-at: u(a),
nh-comp: g ⋅ f,
add-name: I+i,
nc-m: m(i;j)
FDL editor aliases :
fillterm
Latex:
fillterm(Gamma;A;I;i;j;rho;a0;u) ==
\mlambda{}K,f. if isdM0(f i) then (a0 (i0)(rho) s \mcdot{} f) else u(m(i;j) \mcdot{} f) fi
Date html generated:
2016_05_19-AM-09_25_50
Last ObjectModification:
2015_11_08-PM-08_21_58
Theory : cubical!type!theory
Home
Index