Nuprl Definition : sigma-unelim-pscm

SigmaUnElim ==  λI,x. let au,v = x in let a,u = au in (a;(u;v))


Definitions occuring in Statement :  psc-adjoin-set: (v;u),  lambda: λx.A[x],  spread: spread def
Definitions occuring in definition :  lambda: λx.A[x],  spread: spread def,  psc-adjoin-set: (v;u)
FDL editor aliases :  sigma-unelim-pscm
Latex:
SigmaUnElim  ==    \mlambda{}I,x.  let  au,v  =  x  in  let  a,u  =  au  in  (a;(u;v))


Date html generated: 2018_05_23-AM-08_21_40
Last ObjectModification: 2018_02_21-PM-05_51_37

Theory : presheaf!models!of!type!theory


Home Index