Nuprl Definition : pi-meaning
pi-meaning{i:l}(A; B) ==
let Xa,a,ma = A in
let Xb,b,mb = B in
provision(allowed(ma) ∧ allowed(mb); cttType(levl= levelsup(level(allow(ma));level(allow(mb)))
type= Πtype(allow(ma)) type(allow(mb))
comp= pi_comp(context-set(Xa);type(allow(ma));comp(allow(ma));
comp(allow(mb)))))
Definitions occuring in Statement :
context-set: context-set(ctxt),
mk_ctt-type-mng: mk_ctt-type-mng,
ctt-type-comp: comp(T),
ctt-type-type: type(T),
ctt-type-level: level(T),
levelsup: levelsup(x;y),
pi_comp: pi_comp(X;A;cA;cB),
cubical-pi: ΠA B,
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,
mk_ctt-type-mng: mk_ctt-type-mng,
levelsup: levelsup(x;y),
ctt-type-level: level(T),
cubical-pi: ΠA B,
pi_comp: pi_comp(X;A;cA;cB),
context-set: context-set(ctxt),
ctt-type-type: type(T),
ctt-type-comp: comp(T),
allow: Error :allow
Latex:
pi-meaning\{i:l\}(A; B) ==
let Xa,a,ma = A in
let Xb,b,mb = B in
provision(allowed(ma) \mwedge{} allowed(mb); cttType(levl= levelsup(level(allow(ma));level(allow(mb)))
type= \mPi{}type(allow(ma)) type(allow(mb))
comp= pi\_comp(context-set(Xa);type(allow(ma));
comp(allow(ma));comp(allow(mb)))))
Date html generated:
2020_05_21-AM-10_40_53
Last ObjectModification:
2020_05_07-PM-00_24_14
Theory : cubical!type!theory
Home
Index