Nuprl Definition : system-type
system-type(sys) == reduce(λphi_A,B. let phi,A = phi_A in (if phi then A else B);discr(Top);sys)
Definitions occuring in Statement :
case-type: (if phi then A else B),
discrete-cubical-type: discr(T),
reduce: reduce(f;k;as),
top: Top,
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
reduce: reduce(f;k;as),
lambda: λx.A[x],
spread: spread def,
case-type: (if phi then A else B),
discrete-cubical-type: discr(T),
top: Top
FDL editor aliases :
system-type
Latex:
system-type(sys) == reduce(\mlambda{}phi$_{A}$,B. let phi,A = phi$_{A}\mbackslash{}f\000Cf24 in (if phi then A else B);discr(Top);sys)
Date html generated:
2016_05_19-AM-08_50_20
Last ObjectModification:
2016_03_05-PM-08_08_56
Theory : cubical!type!theory
Home
Index