Nuprl Definition : restrict-cubical-context
restrict-cubical-context{i:l}(ctxt;trm) ==
provision(allowed(trm) ∧ type(allow(trm))=𝔽; let X,vs,f = ctxt in
<X, term(allow(trm)), vs, f>)
Definitions occuring in Statement :
ctt-term-term: term(t),
ctt-term-type-is: type(t)=T,
context-subset: Gamma, phi,
face-type: 𝔽,
spreadn: spread3,
pi1: fst(t),
and: P ∧ Q,
pair: <a, b>,
allow: allow(x),
allowed: allowed(x),
provision: provision(ok; v)
Definitions occuring in definition :
provision: Error :provision,
and: P ∧ Q,
allowed: Error :allowed,
ctt-term-type-is: type(t)=T,
pi1: fst(t),
face-type: 𝔽,
spreadn: spread3,
context-subset: Gamma, phi,
ctt-term-term: term(t),
allow: Error :allow,
pair: <a, b>
FDL editor aliases :
restrict-cubical-context
Latex:
restrict-cubical-context\{i:l\}(ctxt;trm) ==
provision(allowed(trm) \mwedge{} type(allow(trm))=\mBbbF{}; let X,vs,f = ctxt in
<X, term(allow(trm)), vs, f>)
Date html generated:
2020_05_20-PM-08_10_59
Last ObjectModification:
2020_05_11-AM-10_26_29
Theory : cubical!type!theory
Home
Index