Nuprl Definition : unglue-meaning
unglue-meaning{i:l}(A; B; C; D; E) ==
let Xa,a,ma = A in
let Xb,b,mb = B in
let Xc,c,mc = C in
let Xd,d,md = D in
let Xe,e,me = E in
provision((allowed(ma) ∧ allowed(mb))
∧ type(allow(mb))=𝔽
∧ (allowed(mc) ∧ allowed(md) ∧ allowed(me))
∧ let A = type(allow(ma)) in
let phi = term(allow(mb)) in
let T = type(allow(mc)) in
let G = fst(allow(me)) in
type(allow(md))=(T ⟶ A) ∧ type(allow(me))=Glue [phi ⊢→ (T;term(allow(md)))] A;
mk-ctt-term-mng(level(allow(ma)); type(allow(ma)); unglue(term(allow(me)))))
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,
unglue-term: unglue(b),
glue-type: Glue [phi ⊢→ (T;w)] A,
context-subset: Gamma, phi,
face-type: 𝔽,
cubical-fun: (A ⟶ B),
let: let,
spreadn: spread3,
pi1: fst(t),
and: P ∧ Q,
allow: allow(x),
allowed: allowed(x),
provision: provision(ok; v)
Definitions occuring in definition :
spreadn: spread3,
provision: Error :provision,
face-type: 𝔽,
allowed: Error :allowed,
let: let,
pi1: fst(t),
and: P ∧ Q,
cubical-fun: (A ⟶ B),
context-subset: Gamma, phi,
ctt-term-type-is: type(t)=T,
glue-type: Glue [phi ⊢→ (T;w)] A,
context-set: context-set(ctxt),
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
ctt-type-level: level(T),
ctt-type-type: type(T),
unglue-term: unglue(b),
ctt-term-term: term(t),
allow: Error :allow
Latex:
unglue-meaning\{i:l\}(A; B; C; D; E) ==
let Xa,a,ma = A in
let Xb,b,mb = B in
let Xc,c,mc = C in
let Xd,d,md = D in
let Xe,e,me = E in
provision((allowed(ma) \mwedge{} allowed(mb))
\mwedge{} type(allow(mb))=\mBbbF{}
\mwedge{} (allowed(mc) \mwedge{} allowed(md) \mwedge{} allowed(me))
\mwedge{} let A = type(allow(ma)) in
let phi = term(allow(mb)) in
let T = type(allow(mc)) in
let G = fst(allow(me)) in
type(allow(md))=(T {}\mrightarrow{} A) \mwedge{} type(allow(me))=Glue [phi \mvdash{}\mrightarrow{} (T;term(allow(md)))] A;
mk-ctt-term-mng(level(allow(ma)); type(allow(ma)); unglue(term(allow(me)))))
Date html generated:
2020_05_21-AM-10_44_49
Last ObjectModification:
2020_05_11-PM-05_21_48
Theory : cubical!type!theory
Home
Index