Nuprl Definition : sigma-unelim-csm
SigmaUnElim == λI,x. let au,v = x in let a,u = au in (a;(u;v))
Definitions occuring in Statement :
cc-adjoin-cube: (v;u),
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
cc-adjoin-cube: (v;u),
spread: spread def,
lambda: λx.A[x]
FDL editor aliases :
sigma-unelim-csm
Latex:
SigmaUnElim == \mlambda{}I,x. let au,v = x in let a,u = au in (a;(u;v))
Date html generated:
2017_01_09-AM-09_17_16
Last ObjectModification:
2016_12_02-AM-11_52_03
Theory : cubical!type!theory
Home
Index