Nuprl Definition : is-cubical-equiv
IsEquiv(T;A;w) == ΠA Contractible(Fiber((w)p;q))
Definitions occuring in Statement :
cubical-fiber: Fiber(w;a),
contractible-type: Contractible(A),
cubical-pi: Π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 :
cubical-pi: ΠA B,
contractible-type: Contractible(A),
cubical-fiber: Fiber(w;a),
cube-context-adjoin: X.A,
csm-ap-type: (AF)s,
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
is-cubical-equiv
is-cubical-equiv
Latex:
IsEquiv(T;A;w) == \mPi{}A Contractible(Fiber((w)p;q))
Date html generated:
2016_06_16-PM-01_55_23
Last ObjectModification:
2016_06_03-PM-02_10_21
Theory : cubical!type!theory
Home
Index