Nuprl Definition : cubical-fiber
Fiber(w;a) == Σ T (Path_(A)p (a)p app((w)p; q))
Definitions occuring in Statement :
path-type: (Path_A a b),
cubical-sigma: Σ A B,
cubical-app: app(w; u),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s
Definitions occuring in definition :
cubical-sigma: Σ A B,
path-type: (Path_A a b),
cube-context-adjoin: X.A,
csm-ap-type: (AF)s,
cubical-app: app(w; u),
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
cubical-fiber
cubical-fiber
Latex:
Fiber(w;a) == \mSigma{} T (Path\_(A)p (a)p app((w)p; q))
Date html generated:
2016_06_16-PM-01_52_32
Last ObjectModification:
2016_06_03-PM-02_07_53
Theory : cubical!type!theory
Home
Index