Nuprl Definition : univalence
Univalence == Πc𝕌 Contractible(Σ c𝕌 Equiv(decode((q)p);decode(q)))
Definitions occuring in Statement :
universe-decode: decode(t),
cubical-universe: c𝕌,
cubical-equiv: Equiv(T;A),
contractible-type: Contractible(A),
cubical-sigma: Σ A B,
cubical-pi: ΠA B,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s
Definitions occuring in definition :
cubical-pi: ΠA B,
contractible-type: Contractible(A),
cubical-sigma: Σ A B,
cubical-equiv: Equiv(T;A),
cube-context-adjoin: X.A,
cubical-universe: c𝕌,
csm-ap-term: (t)s,
cc-fst: p,
universe-decode: decode(t),
cc-snd: q
FDL editor aliases :
univalence
Latex:
Univalence == \mPi{}c\mBbbU{} Contractible(\mSigma{} c\mBbbU{} Equiv(decode((q)p);decode(q)))
Date html generated:
2018_05_23-PM-06_21_07
Last ObjectModification:
2017_11_08-AM-11_00_44
Theory : cubical!type!theory
Home
Index