Nuprl Definition : case-cube
case-cube(phi;A;B;I;rho) == if (phi(rho)==1) then A(rho) else B(rho) fi
Definitions occuring in Statement :
cubical-term-at: u(a),
cubical-type-at: A(a),
fl-eq: (x==y),
face_lattice: face_lattice(I),
lattice-1: 1,
ifthenelse: if b then t else f fi
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
fl-eq: (x==y),
cubical-term-at: u(a),
lattice-1: 1,
face_lattice: face_lattice(I),
cubical-type-at: A(a)
FDL editor aliases :
case-cube
Latex:
case-cube(phi;A;B;I;rho) == if (phi(rho)==1) then A(rho) else B(rho) fi
Date html generated:
2016_05_19-AM-08_41_12
Last ObjectModification:
2016_03_05-PM-07_08_12
Theory : cubical!type!theory
Home
Index