Nuprl Definition : Kan_sigma_filler
Kan_sigma_filler(A;B) ==
λI,alpha,J,x,i,bx. let cubeA = filler(x;i;sigma-box-fst(bx)) in
let cubeB = filler(x;i;sigma-box-snd(bx)) in
<cubeA, cubeB>
Definitions occuring in Statement :
sigma-box-snd: sigma-box-snd(bx),
sigma-box-fst: sigma-box-fst(bx),
Kanfiller: filler(x;i;bx),
cc-adjoin-cube: (v;u),
let: let,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
lambda: λx.A[x],
sigma-box-fst: sigma-box-fst(bx),
let: let,
Kanfiller: filler(x;i;bx),
cc-adjoin-cube: (v;u),
sigma-box-snd: sigma-box-snd(bx),
pair: <a, b>
FDL editor aliases :
Kan_sigma_filler
Latex:
Kan\_sigma\_filler(A;B) ==
\mlambda{}I,alpha,J,x,i,bx. let cubeA = filler(x;i;sigma-box-fst(bx)) in
let cubeB = filler(x;i;sigma-box-snd(bx)) in
<cubeA, cubeB>
Date html generated:
2016_06_16-PM-06_46_58
Last ObjectModification:
2015_09_23-AM-09_32_27
Theory : cubical!sets
Home
Index