Nuprl Definition : path-meaning
path-meaning{i:l}(A; B; C) ==
let Xa,a,ma = A in
let Xb,b,mb = B in
let Xc,c,mc = C in
provision(allowed(ma) ∧ allowed(mb) ∧ allowed(mc) ∧ type(allow(mb))=type(allow(ma)) ∧ type(allow(mc))=type(allow(ma));
cttType(levl= level(allow(ma))
type= (Path_type(allow(ma)) term(allow(mb)) term(allow(mc)))
comp= path_comp(context-set(Xa);type(allow(ma));term(allow(mb));term(allow(mc));
comp(allow(ma)))))
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),
ctt-term-term: term(t),
ctt-term-type-is: type(t)=T,
path_comp: path_comp,
path-type: (Path_A 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,
allowed: Error :allowed,
and: P ∧ Q,
ctt-term-type-is: type(t)=T,
mk_ctt-type-mng: mk_ctt-type-mng,
ctt-type-level: level(T),
path-type: (Path_A a b),
path_comp: path_comp,
context-set: context-set(ctxt),
ctt-type-type: type(T),
ctt-term-term: term(t),
ctt-type-comp: comp(T),
allow: Error :allow
Latex:
path-meaning\{i:l\}(A; B; C) ==
let Xa,a,ma = A in
let Xb,b,mb = B in
let Xc,c,mc = C in
provision(allowed(ma)
\mwedge{} allowed(mb)
\mwedge{} allowed(mc)
\mwedge{} type(allow(mb))=type(allow(ma))
\mwedge{} type(allow(mc))=type(allow(ma));
cttType(levl= level(allow(ma))
type= (Path\_type(allow(ma)) term(allow(mb)) term(allow(mc)))
comp= path\_comp(context-set(Xa);type(allow(ma));term(allow(mb));term(allow(mc));
comp(allow(ma)))))
Date html generated:
2020_05_21-AM-10_41_26
Last ObjectModification:
2020_05_07-PM-02_23_55
Theory : cubical!type!theory
Home
Index