Nuprl Definition : ctt-op-meaning
ctt-op-meaning{i:l}(X; vs; f; L) ==
let k,v = f
in if k =a "nType" then OK(<0, discr(v), discrete_comp(context-set(X);v)>)
if k =a "nterm" then OK(let T,t = v in mk-ctt-term-mng(0; discr(T); discr(t)))
if k =a "opid"
then if v =a "0" then OK(mk-ctt-term-mng(0; 𝕀; 0(𝕀)))
if v =a "1" then OK(mk-ctt-term-mng(0; 𝕀; 1(𝕀)))
if v =a "eq0" then eq0-meaning{i:l}(L[0])
if v =a "eq1" then eq1-meaning{i:l}(L[0])
if v =a "meet" then meet-meaning{i:l}(L[0]; L[1])
if v =a "join" then join-meaning{i:l}(L[0]; L[1])
if v =a "max" then max-meaning{i:l}(L[0]; L[1])
if v =a "min" then min-meaning{i:l}(L[0]; L[1])
if v =a "I" then OK(<0, 𝕀>)
if v =a "F" then OK(cttType(levl= 0type= 𝔽comp= face-comp()))
if v =a "inv" then inv-meaning{i:l}(L[0])
if v =a "sigma" then sigma-meaning{i:l}(L[0]; L[1])
if v =a "pi" then pi-meaning{i:l}(L[0]; L[1])
if v =a "Glue" then Glue-meaning{i:l}(L[0]; L[1]; L[2]; L[3])
if v =a "case" then case-meaning{i:l}(L[0]; L[1]; L[2]; L[3])
if v =a "path" then path-meaning{i:l}(L[0]; L[1]; L[2])
if v =a "decode1" then decode-meaning{i:l}(0; L[0])
if v =a "decode2" then decode-meaning{i:l}(1; L[0])
if v =a "decode3" then decode-meaning{i:l}(2; L[0])
if v =a "encode1" then encode-meaning{i:l}(1; L[0])
if v =a "encode2" then encode-meaning{i:l}(2; L[0])
if v =a "encode3" then encode-meaning{i:l}(3; L[0])
if v =a "pathabs" then pathabs-meaning{i:l}(L[0]; L[1])
if v =a "pathap" then pathapp-meaning{i:l}(L[0]; L[1]; L[2])
if v =a "lambda" then lambda-meaning{i:l}(L[0]; L[1])
if v =a "apply" then apply-meaning{i:l}(L[0]; L[1]; L[2])
if v =a "pair" then pair-meaning{i:l}(L[0]; L[1]; L[2])
if v =a "fst" then fst-meaning{i:l}(L[0]; L[1]; L[2])
if v =a "snd" then snd-meaning{i:l}(L[0]; L[1]; L[2])
if v =a "glue" then glue-meaning{i:l}(L[0]; L[1]; L[2]; L[3])
if v =a "unglue" then unglue-meaning{i:l}(L[0]; L[1]; L[2]; L[3]; L[4])
if v =a "comp" then comp-meaning{i:l}(L[0]; L[1]; L[2]; L[3])
else provision(False; ⋅)
fi
else univ-meaning{i:l}(v)
fi
Definitions occuring in Statement :
univ-meaning: univ-meaning{i:l}(n),
encode-meaning: encode-meaning{i:l}(n; A),
decode-meaning: decode-meaning{i:l}(n; A),
unglue-meaning: unglue-meaning{i:l}(A; B; C; D; E),
glue-meaning: glue-meaning{i:l}(A; B; C; D),
Glue-meaning: Glue-meaning{i:l}(A; B; C; D),
case-meaning: case-meaning{i:l}(A; B; C; D),
comp-meaning: comp-meaning{i:l}(A; B; C; D),
snd-meaning: snd-meaning{i:l}(A; B; C),
fst-meaning: fst-meaning{i:l}(A; B; C),
pair-meaning: pair-meaning{i:l}(A; B; C),
lambda-meaning: lambda-meaning{i:l}(A; B),
apply-meaning: apply-meaning{i:l}(A; B; C),
pathabs-meaning: pathabs-meaning{i:l}(A; B),
pathapp-meaning: pathapp-meaning{i:l}(A; B; C),
path-meaning: path-meaning{i:l}(A; B; C),
sigma-meaning: sigma-meaning{i:l}(A; B),
pi-meaning: pi-meaning{i:l}(A; B),
inv-meaning: inv-meaning{i:l}(A),
min-meaning: min-meaning{i:l}(A; B),
max-meaning: max-meaning{i:l}(A; B),
join-meaning: join-meaning{i:l}(A; B),
meet-meaning: meet-meaning{i:l}(A; B),
eq1-meaning: eq1-meaning{i:l}(Z),
eq0-meaning: eq0-meaning{i:l}(Z),
context-set: context-set(ctxt),
mk_ctt-type-mng: mk_ctt-type-mng,
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
face-comp: face-comp(),
discrete_comp: discrete_comp(G;T),
face-type: 𝔽,
interval-1: 1(𝕀),
interval-0: 0(𝕀),
interval-type: 𝕀,
discrete-cubical-term: discr(t),
discrete-cubical-type: discr(T),
select: L[n],
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
it: ⋅,
false: False,
true: True,
spread: spread def,
pair: <a, b>,
natural_number: $n,
token: "$token",
provision: provision(ok; v)
Definitions occuring in definition :
mk_ctt-type-mng: mk_ctt-type-mng,
true: True,
provision: Error :provision,
token: "$token",
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
interval-type: 𝕀,
natural_number: $n,
pair: <a, b>,
select: L[n],
min-meaning: min-meaning{i:l}(A; B),
max-meaning: max-meaning{i:l}(A; B),
join-meaning: join-meaning{i:l}(A; B),
meet-meaning: meet-meaning{i:l}(A; B),
eq1-meaning: eq1-meaning{i:l}(Z),
eq0-meaning: eq0-meaning{i:l}(Z),
interval-1: 1(𝕀),
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
interval-0: 0(𝕀),
discrete-cubical-term: discr(t),
discrete-cubical-type: discr(T),
spread: spread def,
context-set: context-set(ctxt),
discrete_comp: discrete_comp(G;T),
face-type: 𝔽,
face-comp: face-comp(),
inv-meaning: inv-meaning{i:l}(A),
sigma-meaning: sigma-meaning{i:l}(A; B),
pi-meaning: pi-meaning{i:l}(A; B),
Glue-meaning: Glue-meaning{i:l}(A; B; C; D),
case-meaning: case-meaning{i:l}(A; B; C; D),
path-meaning: path-meaning{i:l}(A; B; C),
decode-meaning: decode-meaning{i:l}(n; A),
pathabs-meaning: pathabs-meaning{i:l}(A; B),
pathapp-meaning: pathapp-meaning{i:l}(A; B; C),
lambda-meaning: lambda-meaning{i:l}(A; B),
apply-meaning: apply-meaning{i:l}(A; B; C),
pair-meaning: pair-meaning{i:l}(A; B; C),
fst-meaning: fst-meaning{i:l}(A; B; C),
snd-meaning: snd-meaning{i:l}(A; B; C),
glue-meaning: glue-meaning{i:l}(A; B; C; D),
unglue-meaning: unglue-meaning{i:l}(A; B; C; D; E),
comp-meaning: comp-meaning{i:l}(A; B; C; D),
false: False,
it: ⋅,
univ-meaning: univ-meaning{i:l}(n)
Latex:
ctt-op-meaning\{i:l\}(X; vs; f; L) ==
let k,v = f
in if k =a "nType" then OK(ɘ, discr(v), discrete\_comp(context-set(X);v)>)
if k =a "nterm" then OK(let T,t = v in mk-ctt-term-mng(0; discr(T); discr(t)))
if k =a "opid"
then if v =a "0" then OK(mk-ctt-term-mng(0; \mBbbI{}; 0(\mBbbI{})))
if v =a "1" then OK(mk-ctt-term-mng(0; \mBbbI{}; 1(\mBbbI{})))
if v =a "eq0" then eq0-meaning\{i:l\}(L[0])
if v =a "eq1" then eq1-meaning\{i:l\}(L[0])
if v =a "meet" then meet-meaning\{i:l\}(L[0]; L[1])
if v =a "join" then join-meaning\{i:l\}(L[0]; L[1])
if v =a "max" then max-meaning\{i:l\}(L[0]; L[1])
if v =a "min" then min-meaning\{i:l\}(L[0]; L[1])
if v =a "I" then OK(ɘ, \mBbbI{}>)
if v =a "F" then OK(cttType(levl= 0type= \mBbbF{}comp= face-comp()))
if v =a "inv" then inv-meaning\{i:l\}(L[0])
if v =a "sigma" then sigma-meaning\{i:l\}(L[0]; L[1])
if v =a "pi" then pi-meaning\{i:l\}(L[0]; L[1])
if v =a "Glue" then Glue-meaning\{i:l\}(L[0]; L[1]; L[2]; L[3])
if v =a "case" then case-meaning\{i:l\}(L[0]; L[1]; L[2]; L[3])
if v =a "path" then path-meaning\{i:l\}(L[0]; L[1]; L[2])
if v =a "decode1" then decode-meaning\{i:l\}(0; L[0])
if v =a "decode2" then decode-meaning\{i:l\}(1; L[0])
if v =a "decode3" then decode-meaning\{i:l\}(2; L[0])
if v =a "encode1" then encode-meaning\{i:l\}(1; L[0])
if v =a "encode2" then encode-meaning\{i:l\}(2; L[0])
if v =a "encode3" then encode-meaning\{i:l\}(3; L[0])
if v =a "pathabs" then pathabs-meaning\{i:l\}(L[0]; L[1])
if v =a "pathap" then pathapp-meaning\{i:l\}(L[0]; L[1]; L[2])
if v =a "lambda" then lambda-meaning\{i:l\}(L[0]; L[1])
if v =a "apply" then apply-meaning\{i:l\}(L[0]; L[1]; L[2])
if v =a "pair" then pair-meaning\{i:l\}(L[0]; L[1]; L[2])
if v =a "fst" then fst-meaning\{i:l\}(L[0]; L[1]; L[2])
if v =a "snd" then snd-meaning\{i:l\}(L[0]; L[1]; L[2])
if v =a "glue" then glue-meaning\{i:l\}(L[0]; L[1]; L[2]; L[3])
if v =a "unglue" then unglue-meaning\{i:l\}(L[0]; L[1]; L[2]; L[3]; L[4])
if v =a "comp" then comp-meaning\{i:l\}(L[0]; L[1]; L[2]; L[3])
else provision(False; \mcdot{})
fi
else univ-meaning\{i:l\}(v)
fi
Date html generated:
2020_05_21-AM-10_45_56
Last ObjectModification:
2020_05_07-PM-04_25_49
Theory : cubical!type!theory
Home
Index