Nuprl Definition : equiv_comp
equiv_comp(H;A;E;cA;cE) ==
sigma_comp(pi_comp(H;A;cA;(cE)p);pi_comp(H.(A ⟶ E);(E)p;(cE)p;contractible_comp(H.(A ⟶ E).(E)p;Fiber((q)p;q);
fiber-comp(H.(A ⟶ E).(E)p;((A)p)p;
((E)p)p;(q)p;q;((cA)p)p;
((cE)p)p))))
Definitions occuring in Statement :
contractible_comp: contractible_comp(X;A;cA),
fiber-comp: fiber-comp(X;T;A;w;a;cT;cA),
pi_comp: pi_comp(X;A;cA;cB),
sigma_comp: sigma_comp(cA;cB),
csm-comp-structure: (cA)tau,
cubical-fiber: Fiber(w;a),
cubical-fun: (A ⟶ B),
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,
cubical-fun: (A ⟶ B),
cube-context-adjoin: X.A,
csm-comp-structure: (cA)tau,
csm-ap-type: (AF)s,
cc-snd: q,
csm-ap-term: (t)s,
fiber-comp: fiber-comp(X;T;A;w;a;cT;cA),
cubical-fiber: Fiber(w;a),
contractible_comp: contractible_comp(X;A;cA),
pi_comp: pi_comp(X;A;cA;cB),
sigma_comp: sigma_comp(cA;cB)
FDL editor aliases :
equiv_comp
Latex:
equiv\_comp(H;A;E;cA;cE) ==
sigma\_comp(pi\_comp(H;A;cA;(cE)p);pi\_comp(H.(A {}\mrightarrow{} E);(E)p;(cE)p;
contractible\_comp(H.(A {}\mrightarrow{} E).(E)p;Fiber((q)p;q);
fiber-comp(H.(A {}\mrightarrow{} E).(E)p;((A)p)p;
((E)p)p;(q)p;q;((cA)p)p;
((cE)p)p))))
Date html generated:
2017_01_10-PM-00_08_57
Last ObjectModification:
2016_12_24-PM-00_28_01
Theory : cubical!type!theory
Home
Index