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