Nuprl Definition : cubical-equiv
Equiv(T;A) == Σ (T ⟶ A) IsEquiv((T)p;(A)p;q)
Definitions occuring in Statement :
is-cubical-equiv: IsEquiv(T;A;w),
cubical-sigma: Σ A B,
cubical-fun: (A ⟶ B),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-type: (AF)s
Definitions occuring in definition :
cubical-sigma: Σ A B,
is-cubical-equiv: IsEquiv(T;A;w),
cube-context-adjoin: X.A,
cubical-fun: (A ⟶ B),
csm-ap-type: (AF)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
cubical-equiv
cubical-equiv
Latex:
Equiv(T;A) == \mSigma{} (T {}\mrightarrow{} A) IsEquiv((T)p;(A)p;q)
Date html generated:
2016_06_16-PM-01_56_05
Last ObjectModification:
2016_06_03-PM-02_10_55
Theory : cubical!type!theory
Home
Index