Nuprl Definition : comp-meaning
comp-meaning{i:l}(A; B; C; D) ==
let Xa,a,ma = A in
let Xb,b,mb = B in
let Xc,c,mc = C in
let Xd,d,md = D in
provision(allowed(ma)
∧ type(allow(ma))=𝔽
∧ allowed(mb)
∧ allowed(mc)
∧ allowed(md)
∧ type(allow(mc))=type(allow(mb))
∧ type(allow(md))=(type(allow(mb)))[0(𝕀)]
∧ ((term(allow(mc)))[0(𝕀)]
= term(allow(md))
∈ {context-set(Xa), term(allow(ma)) ⊢ _:(type(allow(mb)))[0(𝕀)]});
mk-ctt-term-mng(level(allow(mb)); (type(allow(mb)))[1(𝕀)];
comp comp(allow(mb)) [term(allow(ma)) ⊢→ term(allow(mc))] term(allow(md))))
Definitions occuring in Statement :
context-set: context-set(ctxt),
ctt-type-comp: comp(T),
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,
comp_term: comp cA [phi ⊢→ u] a0,
context-subset: Gamma, phi,
face-type: 𝔽,
interval-1: 1(𝕀),
interval-0: 0(𝕀),
interval-type: 𝕀,
csm-id-adjoin: [u],
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
spreadn: spread3,
and: P ∧ Q,
equal: s = t ∈ T,
allow: allow(x),
allowed: allowed(x),
provision: provision(ok; v)
Definitions occuring in definition :
spreadn: spread3,
provision: Error :provision,
face-type: 𝔽,
allowed: Error :allowed,
cube-context-adjoin: X.A,
interval-type: 𝕀,
and: P ∧ Q,
ctt-term-type-is: type(t)=T,
equal: s = t ∈ T,
cubical-term: {X ⊢ _:A},
context-subset: Gamma, phi,
csm-ap-term: (t)s,
interval-0: 0(𝕀),
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],
interval-1: 1(𝕀),
ctt-type-type: type(T),
comp_term: comp cA [phi ⊢→ u] a0,
context-set: context-set(ctxt),
ctt-type-comp: comp(T),
ctt-term-term: term(t),
allow: Error :allow
Latex:
comp-meaning\{i:l\}(A; B; C; D) ==
let Xa,a,ma = A in
let Xb,b,mb = B in
let Xc,c,mc = C in
let Xd,d,md = D in
provision(allowed(ma)
\mwedge{} type(allow(ma))=\mBbbF{}
\mwedge{} allowed(mb)
\mwedge{} allowed(mc)
\mwedge{} allowed(md)
\mwedge{} type(allow(mc))=type(allow(mb))
\mwedge{} type(allow(md))=(type(allow(mb)))[0(\mBbbI{})]
\mwedge{} ((term(allow(mc)))[0(\mBbbI{})] = term(allow(md)));
mk-ctt-term-mng(level(allow(mb)); (type(allow(mb)))[1(\mBbbI{})];
comp comp(allow(mb)) [term(allow(ma)) \mvdash{}\mrightarrow{} term(allow(mc))]
term(allow(md))))
Date html generated:
2020_05_21-AM-10_43_42
Last ObjectModification:
2020_05_13-PM-00_01_02
Theory : cubical!type!theory
Home
Index