Nuprl Definition : cubical-path-1
cubical-path-1(Gamma;A;I;i;rho;phi;u) == {a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)}
Definitions occuring in Statement :
cubical-path-condition': cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1),
cubical-type-at: A(a),
cube-set-restriction: f(s),
nc-1: (i1),
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-1: (i1),
cubical-path-condition': cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)
FDL editor aliases :
cubical-path-1
Latex:
cubical-path-1(Gamma;A;I;i;rho;phi;u) ==
\{a1:A((i1)(rho))| cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)\}
Date html generated:
2016_05_19-AM-09_19_23
Last ObjectModification:
2015_11_03-AM-00_39_32
Theory : cubical!type!theory
Home
Index