Nuprl Definition : fillpath
fillpath(Gamma;A;cA;x;y;z) ==
comp csm-composition(p+;cA) [((q=0) ∨ (q=1)) ⟶ [(q)p=0 ⟶ (app(fill-type-down(Gamma;A;cA); (x)p))p+;
(q)p=1 ⟶ (app(fill-type-up(Gamma;A;cA); (y)p))p+]] z
Definitions occuring in Statement :
fill-type-down: fill-type-down(Gamma;A;cA),
fill-type-up: fill-type-up(Gamma;A;cA),
case-endpoints: [r=0 ⟶ a; r=1 ⟶ b],
composition-term: comp cA [phi ⟶ u] a0,
csm-composition: csm-composition(sigma;comp),
face-zero: (i=0),
face-one: (i=1),
face-or: (a ∨ b),
interval-type: 𝕀,
cubical-app: app(w; u),
csm+: tau+,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s
Definitions occuring in definition :
composition-term: comp cA [phi ⟶ u] a0,
csm-composition: csm-composition(sigma;comp),
face-or: (a ∨ b),
face-zero: (i=0),
face-one: (i=1),
case-endpoints: [r=0 ⟶ a; r=1 ⟶ b],
cc-snd: q,
fill-type-down: fill-type-down(Gamma;A;cA),
csm+: tau+,
cube-context-adjoin: X.A,
interval-type: 𝕀,
cubical-app: app(w; u),
fill-type-up: fill-type-up(Gamma;A;cA),
csm-ap-term: (t)s,
cc-fst: p
FDL editor aliases :
fillpath
Latex:
fillpath(Gamma;A;cA;x;y;z) ==
comp csm-composition(p+;cA) [((q=0) \mvee{} (q=1)) \mvdash{}\mrightarrow{} [(q)p=0 \mvdash{}\mrightarrow{} (app(fill-type-down(Gamma;A;cA);
(x)p))p+;
(q)p=1 \mvdash{}\mrightarrow{} (app(fill-type-up(Gamma;A;cA);
(y)p))p+]] z
Date html generated:
2016_07_08-PM-07_17_13
Last ObjectModification:
2016_06_24-AM-00_10_12
Theory : cubical!type!theory
Home
Index