Nuprl Definition : glue-meaning
glue-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) ∧ allowed(mb))
∧ type(allow(ma))=𝔽
∧ (allowed(mc) ∧ allowed(md))
∧ let phi = term(allow(ma)) in
type(allow(md))=(type(allow(mc)) ⟶ type(allow(mb)))
∧ (app(term(allow(md)); term(allow(mc)))
= term(allow(mb))
∈ {context-set(Xa), phi ⊢ _:type(allow(mb))});
let phi = term(allow(ma)) in
mk-ctt-term-mng(levelsup(level(allow(mb));level(allow(mc)));
Glue [phi ⊢→ (type(allow(mc));term(allow(md)))] type(allow(mb));
glue [phi ⊢→ term(allow(mc))] term(allow(mb))))
Definitions occuring in Statement :
context-set: context-set(ctxt),
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
ctt-term-term: term(t),
ctt-term-type-is: type(t)=T,
ctt-term-type: type(t),
ctt-term-level: level(t),
levelsup: levelsup(x;y),
glue-term: glue [phi ⊢→ t] a,
glue-type: Glue [phi ⊢→ (T;w)] A,
context-subset: Gamma, phi,
face-type: 𝔽,
cubical-app: app(w; u),
cubical-fun: (A ⟶ B),
cubical-term: {X ⊢ _:A},
let: let,
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,
and: P ∧ Q,
ctt-term-type-is: type(t)=T,
cubical-fun: (A ⟶ B),
equal: s = t ∈ T,
cubical-term: {X ⊢ _:A},
context-subset: Gamma, phi,
cubical-app: app(w; u),
let: let,
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
levelsup: levelsup(x;y),
ctt-term-level: level(t),
glue-type: Glue [phi ⊢→ (T;w)] A,
glue-term: glue [phi ⊢→ t] a,
context-set: context-set(ctxt),
ctt-term-type: type(t),
ctt-term-term: term(t),
allow: Error :allow
Latex:
glue-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{} allowed(mb))
\mwedge{} type(allow(ma))=\mBbbF{}
\mwedge{} (allowed(mc) \mwedge{} allowed(md))
\mwedge{} let phi = term(allow(ma)) in
type(allow(md))=(type(allow(mc)) {}\mrightarrow{} type(allow(mb)))
\mwedge{} (app(term(allow(md)); term(allow(mc))) = term(allow(mb)));
let phi = term(allow(ma)) in
mk-ctt-term-mng(levelsup(level(allow(mb));level(allow(mc)));
Glue [phi \mvdash{}\mrightarrow{} (type(allow(mc));term(allow(md)))] type(allow(mb));
glue [phi \mvdash{}\mrightarrow{} term(allow(mc))] term(allow(mb))))
Date html generated:
2020_05_21-AM-10_44_32
Last ObjectModification:
2020_05_12-PM-05_58_28
Theory : cubical!type!theory
Home
Index