Nuprl Definition : univalence-term
univalence-term{i:l}(G; A; B) == equiv-witness(UA;is-equiv-witness(G;(Path_c𝕌 A B);fiber-point(33;44);55))
Definitions occuring in Statement :
univ-a: UA,
cubical-universe: c𝕌,
equiv-witness: equiv-witness(f;cntr),
is-equiv-witness: is-equiv-witness(G;A;c;p),
fiber-point: fiber-point(t;c),
path-type: (Path_A a b),
natural_number: $n
Definitions occuring in definition :
equiv-witness: equiv-witness(f;cntr),
univ-a: UA,
is-equiv-witness: is-equiv-witness(G;A;c;p),
path-type: (Path_A a b),
cubical-universe: c𝕌,
fiber-point: fiber-point(t;c),
natural_number: $n
Latex:
univalence-term\{i:l\}(G; A; B) ==
equiv-witness(UA;is-equiv-witness(G;(Path\_c\mBbbU{} A B);fiber-point(33;44);55))
Date html generated:
2018_05_23-PM-06_26_47
Last ObjectModification:
2017_11_06-PM-06_34_11
Theory : cubical!type!theory
Home
Index