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