Nuprl Definition : univalence_t
univalence_t{i:l}(G) ==
(λbij-contr(G.c𝕌; Σ c𝕌 Equiv(decode((q)p);decode(q)); cubical-sigma-fun(G.c𝕌;c𝕌;Equiv(decode((q)p);decode(q));UA);
cubical-sigma-fun(G.c𝕌;c𝕌;(Path_c𝕌 (q)p q);44); 55; 66; singleton-contr(G.c𝕌;c𝕌;q)))
Definitions occuring in Statement :
univ-a: UA,
universe-decode: decode(t),
cubical-universe: c𝕌,
bij-contr: bij-contr(X; A; f; g; cA; b; c),
singleton-contr: singleton-contr(X;A;a),
cubical-equiv: Equiv(T;A),
path-type: (Path_A a b),
cubical-sigma-fun: cubical-sigma-fun(G;A;B;f),
cubical-sigma: Σ A B,
cubical-lambda: (λb),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
natural_number: $n
Definitions occuring in definition :
cubical-lambda: (λb),
bij-contr: bij-contr(X; A; f; g; cA; b; c),
cubical-sigma: Σ A B,
cubical-equiv: Equiv(T;A),
universe-decode: decode(t),
univ-a: UA,
cubical-sigma-fun: cubical-sigma-fun(G;A;B;f),
path-type: (Path_A a b),
csm-ap-term: (t)s,
cc-fst: p,
natural_number: $n,
singleton-contr: singleton-contr(X;A;a),
cube-context-adjoin: X.A,
cubical-universe: c𝕌,
cc-snd: q
FDL editor aliases :
univalence_t
Latex:
univalence\_t\{i:l\}(G) ==
(\mlambda{}bij-contr(G.c\mBbbU{}; \mSigma{} c\mBbbU{} Equiv(decode((q)p);decode(q));
cubical-sigma-fun(G.c\mBbbU{};c\mBbbU{};Equiv(decode((q)p);decode(q));UA);
cubical-sigma-fun(G.c\mBbbU{};c\mBbbU{};(Path\_c\mBbbU{} (q)p q);44); 55; 66; singleton-contr(G.c\mBbbU{};c\mBbbU{};q)))
Date html generated:
2018_05_23-PM-06_26_31
Last ObjectModification:
2017_11_20-AM-10_20_23
Theory : cubical!type!theory
Home
Index