Nuprl Definition : fiber-comp
fiber-comp(X;T;A;w;a;cT;cA) == sigma_comp(cT;path_comp(X.T;(A)p;(a)p;app((w)p; q);(cA)p))
Definitions occuring in Statement :
path_comp: path_comp(G;A;a;b;cA),
sigma_comp: sigma_comp(cA;cB),
csm-comp-structure: (cA)tau,
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 :
cc-fst: p,
cube-context-adjoin: X.A,
csm-comp-structure: (cA)tau,
cc-snd: q,
csm-ap-term: (t)s,
cubical-app: app(w; u),
csm-ap-type: (AF)s,
path_comp: path_comp(G;A;a;b;cA),
sigma_comp: sigma_comp(cA;cB)
FDL editor aliases :
fiber-comp
Latex:
fiber-comp(X;T;A;w;a;cT;cA) == sigma\_comp(cT;path\_comp(X.T;(A)p;(a)p;app((w)p; q);(cA)p))
Date html generated:
2016_06_16-PM-02_22_17
Last ObjectModification:
2016_06_10-PM-00_56_08
Theory : cubical!type!theory
Home
Index