Nuprl Definition : pathapp-meaning
pathapp-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(mc))=𝕀
∧ ({context-set(Xa) ⊢ _:type(allow(mb))} ⊆r {context-set(Xa) ⊢ _:Path(type(allow(ma)))});
mk-ctt-term-mng(level(allow(ma)); type(allow(ma)); term(allow(mb)) @ term(allow(mc))))
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,
ctt-term-type: type(t),
cubical-path-app: pth @ r,
pathtype: Path(A),
interval-type: 𝕀,
cubical-term: {X ⊢ _:A},
spreadn: spread3,
subtype_rel: A ⊆r B,
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,
interval-type: 𝕀,
subtype_rel: A ⊆r B,
ctt-term-type: type(t),
cubical-term: {X ⊢ _:A},
pathtype: Path(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),
cubical-path-app: pth @ r,
ctt-term-term: term(t),
allow: Error :allow
Latex:
pathapp-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(mc))=\mBbbI{}
\mwedge{} (\{context-set(Xa) \mvdash{} \_:type(allow(mb))\}
\msubseteq{}r \{context-set(Xa) \mvdash{} \_:Path(type(allow(ma)))\});
mk-ctt-term-mng(level(allow(ma)); type(allow(ma)); term(allow(mb)) @ term(allow(mc))))
Date html generated:
2020_05_21-AM-10_41_42
Last ObjectModification:
2020_05_08-AM-00_02_27
Theory : cubical!type!theory
Home
Index