Nuprl Definition : case-type
(if phi then A else B) == <λI,rho. case-cube(phi;A;B;I;rho), λI,J,f,rho,c. if (phi(rho)==1) then (c rho f) else (c rho \000Cf) fi >
Definitions occuring in Statement :
case-cube: case-cube(phi;A;B;I;rho),
cubical-term-at: u(a),
cubical-type-ap-morph: (u a f),
fl-eq: (x==y),
face_lattice: face_lattice(I),
lattice-1: 1,
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
case-cube: case-cube(phi;A;B;I;rho),
lambda: λx.A[x],
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-ap-morph: (u a f)
FDL editor aliases :
case-type
Latex:
(if phi then A else B) ==
<\mlambda{}I,rho. case-cube(phi;A;B;I;rho), \mlambda{}I,J,f,rho,c. if (phi(rho)==1) then (c rho f) else (c rho f) fi\000C >
Date html generated:
2016_05_19-AM-08_41_24
Last ObjectModification:
2016_03_05-PM-07_10_17
Theory : cubical!type!theory
Home
Index