Nuprl Definition : cubical-path-0
cubical-path-0(Gamma;A;I;i;rho;phi;u) == {a0:A((i0)(rho))| cubical-path-condition(Gamma;A;I;i;rho;phi;u;a0)}
Definitions occuring in Statement :
cubical-path-condition: cubical-path-condition(Gamma;A;I;i;rho;phi;u;a0),
cubical-type-at: A(a),
cube-set-restriction: f(s),
nc-0: (i0),
add-name: I+i,
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
cubical-type-at: A(a),
cube-set-restriction: f(s),
add-name: I+i,
nc-0: (i0),
cubical-path-condition: cubical-path-condition(Gamma;A;I;i;rho;phi;u;a0)
FDL editor aliases :
cubical-path-0
Latex:
cubical-path-0(Gamma;A;I;i;rho;phi;u) ==
\{a0:A((i0)(rho))| cubical-path-condition(Gamma;A;I;i;rho;phi;u;a0)\}
Date html generated:
2016_05_19-AM-09_18_48
Last ObjectModification:
2015_11_03-AM-00_20_21
Theory : cubical!type!theory
Home
Index