Nuprl Definition : cubical-contr
cubical-contr(Gamma; A; cA; p; phi; u) == comp csm-composition(p;cA) [phi ⊢→ (app(p.2; u))p @ q] p.1
Definitions occuring in Statement :
composition-term: comp cA [phi ⊢→ u] a0,
csm-composition: csm-composition(sigma;comp),
cubical-path-app: pth @ r,
cubical-snd: p.2,
cubical-fst: p.1,
cubical-app: app(w; u),
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s
Definitions occuring in definition :
composition-term: comp cA [phi ⊢→ u] a0,
csm-composition: csm-composition(sigma;comp),
cubical-path-app: pth @ r,
csm-ap-term: (t)s,
cc-fst: p,
cubical-app: app(w; u),
cubical-snd: p.2,
cc-snd: q,
cubical-fst: p.1
Latex:
cubical-contr(Gamma; A; cA; p; phi; u) ==
comp csm-composition(p;cA) [phi \mvdash{}\mrightarrow{} (app(p.2; u))p @ q] p.1
Date html generated:
2016_06_16-PM-01_58_03
Last ObjectModification:
2016_06_06-PM-04_49_56
Theory : cubical!type!theory
Home
Index