Nuprl Definition : snd-meaning
snd-meaning{i:l}(A; B; C) ==
let Xa,a,ma = A in
let Xb,b,mb = B in
let Xc,c,mc = C in
provision(allowed(ma) ∧ allowed(mb) ∧ allowed(mc) ∧ type(allow(mc))=Σ type(allow(ma)) type(allow(mb));
mk-ctt-term-mng(level(allow(mb)); (type(allow(mb)))[term(allow(mc)).1]; term(allow(mc)).2))
Definitions occuring in Statement :
context-set: context-set(ctxt),
ctt-type-type: type(T),
ctt-type-level: level(T),
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
ctt-term-term: term(t),
ctt-term-type-is: type(t)=T,
cubical-snd: p.2,
cubical-fst: p.1,
cubical-sigma: Σ A B,
csm-id-adjoin: [u],
csm-ap-type: (AF)s,
spreadn: spread3,
and: P ∧ Q,
allow: allow(x),
allowed: allowed(x),
provision: provision(ok; v)
Definitions occuring in definition :
spreadn: spread3,
provision: Error :provision,
and: P ∧ Q,
allowed: Error :allowed,
ctt-term-type-is: type(t)=T,
cubical-sigma: Σ A B,
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
ctt-type-level: level(T),
csm-ap-type: (AF)s,
csm-id-adjoin: [u],
context-set: context-set(ctxt),
cubical-fst: p.1,
ctt-type-type: type(T),
cubical-snd: p.2,
ctt-term-term: term(t),
allow: Error :allow
Latex:
snd-meaning\{i:l\}(A; B; C) ==
let Xa,a,ma = A in
let Xb,b,mb = B in
let Xc,c,mc = C in
provision(allowed(ma)
\mwedge{} allowed(mb)
\mwedge{} allowed(mc)
\mwedge{} type(allow(mc))=\mSigma{} type(allow(ma)) type(allow(mb));
mk-ctt-term-mng(level(allow(mb)); (type(allow(mb)))[term(allow(mc)).1];
term(allow(mc)).2))
Date html generated:
2020_05_21-AM-10_43_23
Last ObjectModification:
2020_05_06-PM-09_52_36
Theory : cubical!type!theory
Home
Index